summaryrefslogtreecommitdiff
path: root/FinMap.agda
diff options
context:
space:
mode:
authorHelmut Grohne <grohne@cs.uni-bonn.de>2014-02-26 09:16:19 +0100
committerHelmut Grohne <grohne@cs.uni-bonn.de>2014-02-26 09:16:19 +0100
commit28e7397a76be229ba723e49db51d2bf0b87c5493 (patch)
tree809131bc5b5afbfc6d6e6a34b957e22a1d0a446c /FinMap.agda
parent8d0659f5dcfec4fc75096aa188c99af35c23bad5 (diff)
downloadbidiragda-28e7397a76be229ba723e49db51d2bf0b87c5493.tar.gz
convert LiftGet module to using heterogeneous equality
The reduction in proof length is impressive.
Diffstat (limited to 'FinMap.agda')
0 files changed, 0 insertions, 0 deletions