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
treedc3ee3e75bc61e1bdefadbbbb59f64ae81331b1e
parent7276a09107901570b11deb6bc18f017a4982a158
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