make more parameters implicit
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 30 Oct 2014 14:05:28 +0000 (15:05 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 30 Oct 2014 14:05:28 +0000 (15:05 +0100)
commita736eed95090ec104edbfbc9ea08bc265c618678
tree6053700c0ae6d5f5e7a81e96c0a1feb6e5f8a33e
parent6fa57da8105a0bad87c571ac911fa54d161745ad
make more parameters implicit

All of these changes were applied to functions of type

... -> (x : ...) -> ... == x -> ...

where x could be preceded by just making the x implicit, because it can
be uniquely deduced from the equality proof.
Bidir.agda
CheckInsert.agda
FinMap.agda
Precond.agda