pass get functions as records
[~helmut/bidiragda.git] / CheckInsert.agda
2014-01-28 Helmut Grohnethere is no need to work with IsPreorder
2014-01-28 Helmut Grohneuse the indexed version of the Vec Setoid
2014-01-27 Helmut GrohneMerge branch feature-delete
2014-01-27 Helmut GrohneMerge branch feature-decsetoid
2014-01-23 Helmut Grohneshow a stronger lemma-checkInsert-restrict
2014-01-17 Helmut Grohnegeneralize checkInsert to arbitrary Setoids
2014-01-16 Helmut Grohnegeneralize lemma-insert-same to arbitrary Setoids
2013-02-01 Helmut Grohneemploy insertionresult in lemma-lookupM-checkInsert
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 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 Grohneadd new lemma-checkInsert-lookupM
2013-01-09 Helmut Grohnesimplify lemma-lookupM-checkInsert using case-split
2012-11-22 Helmut Grohneshorten line length of lemma-lookupM-checkInsert
2012-11-02 Helmut Grohnerewrite checkInsert using "... |" notation
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-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-18 Helmut Grohneone more application of lemma-just\==nnothing
2012-06-05 Helmut Grohnemove checkInsert and related properties to CheckInsert...