2012-09-08 Helmut Grohne give a sufficient precondition for theorem-2 commit | commitdiff | tree | snapshot 2012-09-04 Helmut Grohne rewrite main theorems to using Vec instead of List commit | commitdiff | tree | snapshot 2012-09-04 Helmut Grohne formulate List <-> Vec isomorphism problems commit | commitdiff | tree | snapshot 2012-08-30 Helmut Grohne prove LiftGet.get-trafo-2-getlen commit | commitdiff | tree | snapshot 2012-08-30 Helmut Grohne phrase other half of bijection in LiftGet commit | commitdiff | tree | snapshot 2012-08-30 Helmut Grohne prove half of the bijection in LiftGet commit | commitdiff | tree | snapshot 2012-08-30 Helmut Grohne give the type of different gets a name commit | commitdiff | tree | snapshot 2012-08-06 Helmut Grohne attempt isomorphism between get on List and on Vec commit | commitdiff | tree | snapshot 2012-06-19 Helmut Grohne third definition of bff commit | commitdiff | tree | snapshot 2012-06-05 Helmut Grohne make the Vec bff more similar to the List version commit | commitdiff | tree | snapshot 2012-06-05 Helmut Grohne define a bff over Vec commit | commitdiff | tree | snapshot 2012-06-05 Helmut Grohne move bff and friends to submodule ListBFF commit | commitdiff | tree | snapshot 2012-06-05 Helmut Grohne move checkInsert and related properties to CheckInsert... commit | commitdiff | tree | snapshot 2012-04-27 Helmut Grohne lemma-2: do not confuse lookup with lookupM commit | commitdiff | tree | snapshot 2012-04-27 Helmut Grohne use fromFunc to define union commit | commitdiff | tree | snapshot 2012-04-27 Helmut Grohne prove the theorem-2 commit | commitdiff | tree | snapshot 2012-04-20 Helmut Grohne remove lemma-\in-lookupM-assoc commit | commitdiff | tree | snapshot 2012-04-20 Helmut Grohne complete lemma-2 using new property _in-domain-of_ commit | commitdiff | tree | snapshot 2012-04-19 Helmut Grohne reduce hole in lemma-2 commit | commitdiff | tree | snapshot 2012-04-19 Helmut Grohne FinMap: lemma-lookupM-restrict drop useless implicit commit | commitdiff | tree | snapshot 2012-04-19 Helmut Grohne move lemma-just!=nothing to FinMap and use it there commit | commitdiff | tree | snapshot 2012-04-17 Helmut Grohne inline bot-elim into lemma-just-nothing commit | commitdiff | tree | snapshot 2012-04-04 Helmut Grohne abstract proofs over checkInsert commit | commitdiff | tree | snapshot 2012-03-16 Helmut Grohne fix wrong function name in lemma-2 commit | commitdiff | tree | snapshot 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