2012-02-09 Helmut Grohne remove useless braces commit | commitdiff | tree | snapshot 2012-02-09 Helmut Grohne avoid a sym in lemma-union-restrict commit | commitdiff | tree | snapshot 2012-02-09 Helmut Grohne s/generate/restrict/g commit | commitdiff | tree | snapshot 2012-02-09 Helmut Grohne rephrase free-theorem-list-list using pointwise equality commit | commitdiff | tree | snapshot 2012-02-09 Helmut Grohne formulate theorem-2 commit | commitdiff | tree | snapshot 2012-02-09 Helmut Grohne prove lemma-union-generate commit | commitdiff | tree | snapshot 2012-02-09 Helmut Grohne prove theorem-1 assuming a lemma-union-generate commit | commitdiff | tree | snapshot 2012-02-09 Helmut Grohne started proving theorem-1 commit | commitdiff | tree | snapshot 2012-02-09 Helmut Grohne introduce denumerate commit | commitdiff | tree | snapshot 2012-01-31 Helmut Grohne replace idrange with enumerate commit | commitdiff | tree | snapshot 2012-01-31 Helmut Grohne postulate free theorem for List a -> List a commit | commitdiff | tree | snapshot 2012-01-26 Helmut Grohne recursion of lemma-2 commit | commitdiff | tree | snapshot 2012-01-26 Helmut Grohne started proving lemma-2 commit | commitdiff | tree | snapshot 2012-01-26 Helmut Grohne reduce imports to speed up agda-mode commit | commitdiff | tree | snapshot 2012-01-26 Helmut Grohne split Bidir.agda to FinMap.agda commit | commitdiff | tree | snapshot 2012-01-26 Helmut Grohne improve readability using spaces commit | commitdiff | tree | snapshot 2012-01-26 Helmut Grohne reduce usage of sym commit | commitdiff | tree | snapshot 2012-01-26 Helmut Grohne open \==-Reasoning at top level commit | commitdiff | tree | snapshot 2012-01-26 Helmut Grohne prove the remaining parts of lemma-checkInsert-generate commit | commitdiff | tree | snapshot 2012-01-26 Helmut Grohne complete the yes part of lemma-checkInsert-generate... commit | commitdiff | tree | snapshot 2012-01-26 Helmut Grohne change lemma-insert-same to work with \== proofs commit | commitdiff | tree | snapshot 2012-01-23 Helmut Grohne base case of lemma-2 commit | commitdiff | tree | snapshot 2012-01-23 Helmut Grohne rewrite lemma-1 using propositional equality commit | commitdiff | tree | snapshot 2012-01-22 Helmut Grohne actually fmap is what I meant instead of >>= commit | commitdiff | tree | snapshot 2012-01-22 Helmut Grohne introduce >>= on Maybe to improve readability commit | commitdiff | tree | snapshot 2012-01-22 Helmut Grohne improve readability by introducing EqInst commit | commitdiff | tree | snapshot 2012-01-22 Helmut Grohne formulate theorem-1 commit | commitdiff | tree | snapshot 2012-01-22 Helmut Grohne formulate lemma-2 commit | commitdiff | tree | snapshot 2012-01-22 Helmut Grohne attempt to prove lemma-1 commit | commitdiff | tree | snapshot 2012-01-21 Helmut Grohne rewrite generate using zip and fromAscList commit | commitdiff | tree | snapshot 2012-01-21 Helmut Grohne split FinMap to FinMapMaybe commit | commitdiff | tree | snapshot 2012-01-19 Helmut Grohne replaced NatMap with FinMap commit | commitdiff | tree | snapshot 2012-01-19 Helmut Grohne first attempt to define bff (with holes) commit | commitdiff | tree | snapshot 2012-01-19 Helmut Grohne employ standard library of agda where possible commit | commitdiff | tree | snapshot 2012-01-19 Helmut Grohne first attempt to model lemma-1 commit | commitdiff | tree | snapshot 2012-01-19 Helmut Grohne added .gitignore commit | commitdiff | tree | snapshot