projects / ~helmut / bidiragda.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b2eb5ee) | patch
remove lemma-\in-lookupM-assoc
authorHelmut Grohne <helmut@subdivi.de>
Fri, 20 Apr 2012 10:15:33 +0000 (12:15 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Fri, 20 Apr 2012 10:15:33 +0000 (12:15 +0200)
commit1a8af12f97732cf087264f79483ee1d9aa035b3d
tree50a9a41ac4aaf876cb053b988ff4d51c5d114050tree | snapshot
parentb2eb5eef26787fcb9ff0778f82473b0fc2dc4caacommit | diff
remove lemma-\in-lookupM-assoc

It is a special case of lemma-assoc-domain.
Bidir.agda diff | blob | history
Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)