diff options
author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-10-30 15:05:28 +0100 |
---|---|---|
committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-10-30 15:05:28 +0100 |
commit | a736eed95090ec104edbfbc9ea08bc265c618678 (patch) | |
tree | 6053700c0ae6d5f5e7a81e96c0a1feb6e5f8a33e /Generic.agda | |
parent | 6fa57da8105a0bad87c571ac911fa54d161745ad (diff) | |
download | bidiragda-a736eed95090ec104edbfbc9ea08bc265c618678.tar.gz |
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.
Diffstat (limited to 'Generic.agda')
0 files changed, 0 insertions, 0 deletions