20140128 
Helmut Grohne  improve readability using _∋_≈_ instead of Setoid._≈_ 
blob  commitdiff 
20140128 
Helmut Grohne  use the indexed version of the Vec Setoid 
blob  commitdiff  diff to current 
20140128 
Helmut Grohne  cleanup unused function and import 
blob  commitdiff  diff to current 
20140127 
Helmut Grohne  Merge branch featuredelete 
blob  commitdiff  diff to current 
20140127 
Helmut Grohne  Merge branch featuredecsetoid 
blob  commitdiff  diff to current 
20140127 
Helmut Grohne  cleanup unused functions and useless steps 
blob  commitdiff  diff to current 
20140124 
Helmut Grohne  prove theorem2 in the presence of delete 
blob  commitdiff  diff to current 
20140123 
Helmut Grohne  generalize BFF and theorem2 to arbitrary Setoids 
blob  commitdiff  diff to current 
20140123 
Helmut Grohne  show a stronger lemmacheckInsertrestrict 
blob  commitdiff  diff to current 
20140117 
Helmut Grohne  generalize checkInsert to arbitrary Setoids 
blob  commitdiff  diff to current 
20131217 
Helmut Grohne  refactor to get rid of FinMap without Maybe entirely 
blob  commitdiff  diff to current 
20131217 
Helmut Grohne  update bff implementation to use delete 
blob  commitdiff  diff to current 
20131216 
Helmut Grohne  move generic functions to a new Generic module 
blob  commitdiff  diff to current 
20131002 
Helmut Grohne  need to fully qualify Data.List.All._::_ 
blob  commitdiff  diff to current 
20130721 
Helmut Grohne  import _>>=_ and fmap from Data.Maybe 
blob  commitdiff  diff to current 
20130419 
Helmut Grohne  move lemma\notinlookupMassoc to Precond 
blob  commitdiff  diff to current 
20130410 
Helmut Grohne  lemmamaplookupMassoc is even simpler 
blob  commitdiff  diff to current 
20130409 
Helmut Grohne  rewrite lemmamaplookupMassoc 
blob  commitdiff  diff to current 
20130128 
Helmut Grohne  drop the insert prefix from the insertionresult ctors 
blob  commitdiff  diff to current 
20130117 
Helmut Grohne  Merge branch view2 into master 
blob  commitdiff  diff to current 
20130114 
Helmut Grohne  shrink lemmaunionnotused by matching on All's ctor 
blob  commitdiff  diff to current 
20130114 
Helmut Grohne  define a more useful version of lemmajust\==nnothing 
blob  commitdiff  diff to current 
20130112 
Helmut Grohne  introduce a proper view on checkInsert 
blob  commitdiff  diff to current 
20130110 
Helmut Grohne  Merge branch 'newlemma' 
blob  commitdiff  diff to current 
20130110 
Helmut Grohne  reduce a precondition of lemmacheckInsertlookupM 
blob  commitdiff  diff to current 
20130109 
Helmut Grohne  rewrite lemma\notinlookupMassoc 
blob  commitdiff  diff to current 
20130105 
Helmut Grohne  shrink lemmaunionnotused using cong\_2 
blob  commitdiff  diff to current 
20130105 
Helmut Grohne  shrink lemmamaplookupMinsert using cong\_2 
blob  commitdiff  diff to current 
20130105 
Helmut Grohne  shrink base case of lemma/notinlookupMassoc 
blob  commitdiff  diff to current 
20121210 
Helmut Grohne  drop unused import 
blob  commitdiff  diff to current 
20121210 
Helmut Grohne  drop unused param from lemmamaplookupMinsert 
blob  commitdiff  diff to current 
20121206 
Helmut Grohne  reduce useless case in lemmamaplookupMassoc 
blob  commitdiff  diff to current 
20121122 
Helmut Grohne  shorten line lengths of theorem2 
blob  commitdiff  diff to current 
20121122 
Helmut Grohne  shorten line length of theorem1 
blob  commitdiff  diff to current 
20121119 
Helmut Grohne  turn lemmafmapjust parameter into implicit 
blob  commitdiff  diff to current 
20121117 
Helmut Grohne  strip prose from lemma1 and lemma2 
blob  commitdiff  diff to current 
20121025 
Helmut Grohne  similarly rename lemmafrommapjust to mapjustinjective 
blob  commitdiff  diff to current 
20121025 
Helmut Grohne  rename lemmafromjust to justinjective 
blob  commitdiff  diff to current 
20121022 
Helmut Grohne  Merge branch 'modparam' 
blob  commitdiff  diff to current 
20121022 
Helmut Grohne  finally parameterize CheckInsert 
blob  commitdiff  diff to current 
20121022 
Helmut Grohne  now parameterize BFF 
blob  commitdiff  diff to current 
20121022 
Helmut Grohne  parameterize Bidir via Carrier and deq 
blob  commitdiff  diff to current 
20121005 
Helmut Grohne  move all postulates to one module 
blob  commitdiff  diff to current 
20120927 
Helmut Grohne  move definition of gettype to BFF and use it everywhere 
blob  commitdiff  diff to current 
20120926 
Helmut Grohne  use _\==n_ and _\notin_ instead of \neg 
blob  commitdiff  diff to current 
20120926 
Helmut Grohne  import [_] instead of Reveal_is_ 
blob  commitdiff  diff to current 
20120918 
Helmut Grohne  Merge branch 'usingvec' 
blob  commitdiff  diff to current 
20120917 
Helmut Grohne  save a with in lemma\innlookupMassoc 
blob  commitdiff  diff to current 
20120914 
Helmut Grohne  employ rewrite in lemmamaplookupMassoc 
blob  commitdiff  diff to current 
20120904 
Helmut Grohne  rewrite main theorems to using Vec instead of List 
blob  commitdiff  diff to current 
20120605 
Helmut Grohne  move bff and friends to submodule ListBFF 
blob  commitdiff  diff to current 
20120605 
Helmut Grohne  move checkInsert and related properties to CheckInsert... 
blob  commitdiff  diff to current 
20120427 
Helmut Grohne  lemma2: do not confuse lookup with lookupM 
blob  commitdiff  diff to current 
20120427 
Helmut Grohne  prove the theorem2 
blob  commitdiff  diff to current 
20120420 
Helmut Grohne  remove lemma\inlookupMassoc 
blob  commitdiff  diff to current 
20120420 
Helmut Grohne  complete lemma2 using new property _indomainof_ 
blob  commitdiff  diff to current 
20120419 
Helmut Grohne  reduce hole in lemma2 
blob  commitdiff  diff to current 
20120419 
Helmut Grohne  move lemmajust!=nothing to FinMap and use it there 
blob  commitdiff  diff to current 
20120417 
Helmut Grohne  inline botelim into lemmajustnothing 
blob  commitdiff  diff to current 
20120404 
Helmut Grohne  abstract proofs over checkInsert 
blob  commitdiff  diff to current 
20120316 
Helmut Grohne  fix wrong function name in lemma2 
blob  commitdiff  diff to current 
20120209 
Helmut Grohne  remove useless braces 
blob  commitdiff  diff to current 
20120209 
Helmut Grohne  s/generate/restrict/g 
blob  commitdiff  diff to current 
20120209 
Helmut Grohne  rephrase freetheoremlistlist using pointwise equality 
blob  commitdiff  diff to current 
20120209 
Helmut Grohne  formulate theorem2 
blob  commitdiff  diff to current 
20120209 
Helmut Grohne  prove lemmauniongenerate 
blob  commitdiff  diff to current 
20120209 
Helmut Grohne  prove theorem1 assuming a lemmauniongenerate 
blob  commitdiff  diff to current 
20120209 
Helmut Grohne  started proving theorem1 
blob  commitdiff  diff to current 
20120209 
Helmut Grohne  introduce denumerate 
blob  commitdiff  diff to current 
20120131 
Helmut Grohne  replace idrange with enumerate 
blob  commitdiff  diff to current 
20120131 
Helmut Grohne  postulate free theorem for List a > List a 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  recursion of lemma2 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  started proving lemma2 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  reduce imports to speed up agdamode 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  split Bidir.agda to FinMap.agda 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  improve readability using spaces 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  reduce usage of sym 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  open \==Reasoning at top level 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  prove the remaining parts of lemmacheckInsertgenerate 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  complete the yes part of lemmacheckInsertgenerate... 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  change lemmainsertsame to work with \== proofs 
blob  commitdiff  diff to current 
20120123 
Helmut Grohne  base case of lemma2 
blob  commitdiff  diff to current 
20120123 
Helmut Grohne  rewrite lemma1 using propositional equality 
blob  commitdiff  diff to current 
20120122 
Helmut Grohne  actually fmap is what I meant instead of >>= 
blob  commitdiff  diff to current 
20120122 
Helmut Grohne  introduce >>= on Maybe to improve readability 
blob  commitdiff  diff to current 
20120122 
Helmut Grohne  improve readability by introducing EqInst 
blob  commitdiff  diff to current 
20120122 
Helmut Grohne  formulate theorem1 
blob  commitdiff  diff to current 
20120122 
Helmut Grohne  formulate lemma2 
blob  commitdiff  diff to current 
20120122 
Helmut Grohne  attempt to prove lemma1 
blob  commitdiff  diff to current 
20120121 
Helmut Grohne  rewrite generate using zip and fromAscList 
blob  commitdiff  diff to current 
20120121 
Helmut Grohne  split FinMap to FinMapMaybe 
blob  commitdiff  diff to current 
20120119 
Helmut Grohne  replaced NatMap with FinMap 
blob  commitdiff  diff to current 
20120119 
Helmut Grohne  first attempt to define bff (with holes) 
blob  commitdiff  diff to current 
20120119 
Helmut Grohne  employ standard library of agda where possible 
blob  commitdiff  diff to current 
20120119 
Helmut Grohne  first attempt to model lemma1 
blob  commitdiff  diff to current 
