first attempt to model lemma-1
authorHelmut Grohne <helmut@subdivi.de>
Thu, 19 Jan 2012 10:33:17 +0000 (11:33 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Thu, 19 Jan 2012 10:33:17 +0000 (11:33 +0100)
commit537a03c250380225285be4cba1d05cacfd71ab44
tree627c769009188a069e21ee7488309bb1ae47b87e
parent627abd640e94159ccdc5c6615fbbca347ade3b63
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.
Bidir.agda [new file with mode: 0644]