formulate theorem-2
[~helmut/bidiragda.git] / Bidir.agda
2012-02-09 Helmut Grohneformulate theorem-2
2012-02-09 Helmut Grohneprove lemma-union-generate
2012-02-09 Helmut Grohneprove theorem-1 assuming a lemma-union-generate
2012-02-09 Helmut Grohnestarted proving theorem-1
2012-02-09 Helmut Grohneintroduce denumerate
2012-01-31 Helmut Grohnereplace idrange with enumerate
2012-01-31 Helmut Grohnepostulate free theorem for List a -> List a
2012-01-26 Helmut Grohnerecursion of lemma-2
2012-01-26 Helmut Grohnestarted proving lemma-2
2012-01-26 Helmut Grohnereduce imports to speed up agda-mode
2012-01-26 Helmut Grohnesplit Bidir.agda to FinMap.agda
2012-01-26 Helmut Grohneimprove readability using spaces
2012-01-26 Helmut Grohnereduce usage of sym
2012-01-26 Helmut Grohneopen \==-Reasoning at top level
2012-01-26 Helmut Grohneprove the remaining parts of lemma-checkInsert-generate
2012-01-26 Helmut Grohnecomplete the yes part of lemma-checkInsert-generate...
2012-01-26 Helmut Grohnechange lemma-insert-same to work with \== proofs
2012-01-23 Helmut Grohnebase case of lemma-2
2012-01-23 Helmut Grohnerewrite lemma-1 using propositional equality
2012-01-22 Helmut Grohneactually fmap is what I meant instead of >>=
2012-01-22 Helmut Grohneintroduce >>= on Maybe to improve readability
2012-01-22 Helmut Grohneimprove readability by introducing EqInst
2012-01-22 Helmut Grohneformulate theorem-1
2012-01-22 Helmut Grohneformulate lemma-2
2012-01-22 Helmut Grohneattempt to prove lemma-1
2012-01-21 Helmut Grohnerewrite generate using zip and fromAscList
2012-01-21 Helmut Grohnesplit FinMap to FinMapMaybe
2012-01-19 Helmut Grohnereplaced NatMap with FinMap
2012-01-19 Helmut Grohnefirst attempt to define bff (with holes)
2012-01-19 Helmut Grohneemploy standard library of agda where possible
2012-01-19 Helmut Grohnefirst attempt to model lemma-1