trim lemma-union-restrict
[~helmut/bidiragda.git] / Bidir.agda
2013-04-10 Helmut Grohnelemma-map-lookupM-assoc is even simpler
2013-04-09 Helmut Grohnerewrite lemma-map-lookupM-assoc
2013-01-28 Helmut Grohnedrop the insert- prefix from the insertionresult ctors
2013-01-17 Helmut GrohneMerge branch view2 into master
2013-01-14 Helmut Grohneshrink lemma-union-not-used by matching on All's ctor
2013-01-14 Helmut Grohnedefine a more useful version of lemma-just\==nnothing
2013-01-12 Helmut Grohneintroduce a proper view on checkInsert
2013-01-10 Helmut GrohneMerge branch 'newlemma'
2013-01-10 Helmut Grohnereduce a precondition of lemma-checkInsert-lookupM
2013-01-09 Helmut Grohnerewrite lemma-\notin-lookupM-assoc
2013-01-05 Helmut Grohneshrink lemma-union-not-used using cong\_2
2013-01-05 Helmut Grohneshrink lemma-map-lookupM-insert using cong\_2
2013-01-05 Helmut Grohneshrink base case of lemma-/notin-lookupM-assoc
2012-12-10 Helmut Grohnedrop unused import
2012-12-10 Helmut Grohnedrop unused param from lemma-map-lookupM-insert
2012-12-06 Helmut Grohnereduce useless case in lemma-map-lookupM-assoc
2012-11-22 Helmut Grohneshorten line lengths of theorem-2
2012-11-22 Helmut Grohneshorten line length of theorem-1
2012-11-19 Helmut Grohneturn lemma-fmap-just parameter into implicit
2012-11-17 Helmut Grohnestrip prose from lemma-1 and lemma-2
2012-10-25 Helmut Grohnesimilarly rename lemma-from-map-just to map-just-injective
2012-10-25 Helmut Grohnerename lemma-from-just to just-injective
2012-10-22 Helmut GrohneMerge branch 'modparam'
2012-10-22 Helmut Grohnefinally parameterize CheckInsert
2012-10-22 Helmut Grohnenow parameterize BFF
2012-10-22 Helmut Grohneparameterize Bidir via Carrier and deq
2012-10-05 Helmut Grohnemove all postulates to one module
2012-09-27 Helmut Grohnemove definition of get-type to BFF and use it everywhere
2012-09-26 Helmut Grohneuse _\==n_ and _\notin_ instead of \neg
2012-09-26 Helmut Grohneimport [_] instead of Reveal_is_
2012-09-18 Helmut GrohneMerge branch 'using-vec'
2012-09-17 Helmut Grohnesave a with in lemma-\inn-lookupM-assoc
2012-09-14 Helmut Grohneemploy rewrite in lemma-map-lookupM-assoc
2012-09-04 Helmut Grohnerewrite main theorems to using Vec instead of List
2012-06-05 Helmut Grohnemove bff and friends to submodule ListBFF
2012-06-05 Helmut Grohnemove checkInsert and related properties to CheckInsert...
2012-04-27 Helmut Grohnelemma-2: do not confuse lookup with lookupM
2012-04-27 Helmut Grohneprove the theorem-2
2012-04-20 Helmut Grohneremove lemma-\in-lookupM-assoc
2012-04-20 Helmut Grohnecomplete lemma-2 using new property _in-domain-of_
2012-04-19 Helmut Grohnereduce hole in lemma-2
2012-04-19 Helmut Grohnemove lemma-just!=nothing to FinMap and use it there
2012-04-17 Helmut Grohneinline bot-elim into lemma-just-nothing
2012-04-04 Helmut Grohneabstract proofs over checkInsert
2012-03-16 Helmut Grohnefix wrong function name in lemma-2
2012-02-09 Helmut Grohneremove useless braces
2012-02-09 Helmut Grohnes/generate/restrict/g
2012-02-09 Helmut Grohnerephrase free-theorem-list-list using pointwise equality
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