projects / ~helmut / bidiragda.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7276a09) | patch
replaced NatMap with FinMap
authorHelmut Grohne <helmut@subdivi.de>
Thu, 19 Jan 2012 11:27:53 +0000 (12:27 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Thu, 19 Jan 2012 11:27:53 +0000 (12:27 +0100)
commitce0fc8fe4e14491e52e796d2ddbaa07d90060697
treedc3ee3e75bc61e1bdefadbbbb59f64ae81331b1etree | snapshot
parent7276a09107901570b11deb6bc18f017a4982a158commit | diff
replaced NatMap with FinMap

The domain of the map is always limited. So using Fin n as the domain is
natural. Additionally FinMaps are now semantically equal iff their normal form
is the same. That means \== can be used.
Bidir.agda diff | blob | history
Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)