projects / ~helmut / bidiragda.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ce0fc8f) | patch
split FinMap to FinMapMaybe
authorHelmut Grohne <helmut@subdivi.de>
Sat, 21 Jan 2012 09:58:14 +0000 (10:58 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Sat, 21 Jan 2012 09:58:14 +0000 (10:58 +0100)
commit6e458b738fd75fccac1c605091bfcf7486001533
tree3cbb7002ae371e3c979ccdfd366fe067bef938b4tree | snapshot
parentce0fc8fe4e14491e52e796d2ddbaa07d90060697commit | diff
split FinMap to FinMapMaybe

The FinMapMaybe is what FinMap previously was. The FinMap instead now really
maps its whole domain to something. This property is needed to avoid the
usage of fromJust in the definition of bff. With this split applied the
definition of bff is now complete.
Bidir.agda diff | blob | history
Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)