projects / ~helmut / bidiragda.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6fa57da) | patch
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
tree6053700c0ae6d5f5e7a81e96c0a1feb6e5f8a33etree | snapshot
parent6fa57da8105a0bad87c571ac911fa54d161745adcommit | diff
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 diff | blob | history
CheckInsert.agda diff | blob | history
FinMap.agda diff | blob | history
Precond.agda diff | blob | history
Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)