summaryrefslogtreecommitdiff
path: root/Instances.agda
diff options
context:
space:
mode:
authorHelmut Grohne <grohne@cs.uni-bonn.de>2014-10-30 15:05:28 +0100
committerHelmut Grohne <grohne@cs.uni-bonn.de>2014-10-30 15:05:28 +0100
commita736eed95090ec104edbfbc9ea08bc265c618678 (patch)
tree6053700c0ae6d5f5e7a81e96c0a1feb6e5f8a33e /Instances.agda
parent6fa57da8105a0bad87c571ac911fa54d161745ad (diff)
downloadbidiragda-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 'Instances.agda')
0 files changed, 0 insertions, 0 deletions