change restrict and fromAscList to work with Vec
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 20 Oct 2014 15:01:38 +0000 (17:01 +0200)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 20 Oct 2014 15:04:10 +0000 (17:04 +0200)
commit2991f01c1867d6431d50d0e1309522b005de4bde
treecc7cb093ff2d59d04a861038c13b8fcbb5d260d2
parent58bce3d887d1e5fef24254098819dd09e900fb4c
change restrict and fromAscList to work with Vec

While they do work with Lists and there is no inherent need to know the
length, they are most often invoked in a context where a Vec needs to be
converted to a List using toList. By changing them to work with Vec,
quite a few toList calls can be dropped.
Bidir.agda
CheckInsert.agda
FinMap.agda