10 years agosplit FinMap to FinMapMaybe
Helmut Grohne [Sat, 21 Jan 2012 09:58:14 +0000 (10:58 +0100)]
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.

10 years agoreplaced NatMap with FinMap
Helmut Grohne [Thu, 19 Jan 2012 11:27:53 +0000 (12:27 +0100)]
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.

10 years agofirst attempt to define bff (with holes)
Helmut Grohne [Thu, 19 Jan 2012 11:11:01 +0000 (12:11 +0100)]
first attempt to define bff (with holes)

10 years agoemploy standard library of agda where possible
Helmut Grohne [Thu, 19 Jan 2012 10:47:16 +0000 (11:47 +0100)]
employ standard library of agda where possible

10 years agofirst attempt to model lemma-1
Helmut Grohne [Thu, 19 Jan 2012 10:33:17 +0000 (11:33 +0100)]
first attempt to model lemma-1

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.

10 years agoadded .gitignore
Helmut Grohne [Thu, 19 Jan 2012 10:31:52 +0000 (11:31 +0100)]
added .gitignore