projects / ~helmut / bidiragda.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8d0659f) | patch
convert LiftGet module to using heterogeneous equality
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Wed, 26 Feb 2014 08:16:19 +0000 (09:16 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Wed, 26 Feb 2014 08:16:19 +0000 (09:16 +0100)
commit28e7397a76be229ba723e49db51d2bf0b87c5493
tree809131bc5b5afbfc6d6e6a34b957e22a1d0a446ctree | snapshot
parent8d0659f5dcfec4fc75096aa188c99af35c23bad5commit | diff
convert LiftGet module to using heterogeneous equality

The reduction in proof length is impressive.
LiftGet.agda diff | blob | history
Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)