~helmut/bidiragda.git
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