| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
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.
|
|
|
|
|
|
Without using the stdlib basic data structures are defined (with the
stdlib names in mind). The IntMap given in the paper is translated to a
NatMap. There are definitions for checkInsert and assoc resulting in a
formalization of lemma-1.
|
|
|
