summaryrefslogtreecommitdiff
path: root/CheckInsert.agda
AgeCommit message (Expand)Author
2014-11-26fix compilation against agda stdlib 0.9Helmut Grohne
2014-10-30make more parameters implicitHelmut Grohne
2014-10-20change restrict and fromAscList to work with VecHelmut Grohne
2014-10-16sym result of lemma-lookupM-{i,checkI}nsert-otherHelmut Grohne
2014-10-15remove lemma-just≢nothingHelmut Grohne
2014-01-28there is no need to work with IsPreorderHelmut Grohne
2014-01-28use the indexed version of the Vec SetoidHelmut Grohne
2014-01-23show a stronger lemma-checkInsert-restrictHelmut Grohne
2014-01-17generalize checkInsert to arbitrary SetoidsHelmut Grohne
2014-01-16generalize lemma-insert-same to arbitrary SetoidsHelmut Grohne
2013-02-01employ insertionresult in lemma-lookupM-checkInsertHelmut Grohne
2013-01-28drop the insert- prefix from the insertionresult ctorsHelmut Grohne
2013-01-17Merge branch view2 into masterHelmut Grohne
2013-01-14define a more useful version of lemma-just\==nnothingHelmut Grohne
2013-01-12introduce a proper view on checkInsertHelmut Grohne
2013-01-10reduce a precondition of lemma-checkInsert-lookupMHelmut Grohne
2013-01-10add new lemma-checkInsert-lookupMHelmut Grohne
2013-01-09simplify lemma-lookupM-checkInsert using case-splitHelmut Grohne
2012-11-22shorten line length of lemma-lookupM-checkInsertHelmut Grohne
2012-11-02rewrite checkInsert using "... |" notationHelmut Grohne
2012-10-25rename lemma-from-just to just-injectiveHelmut Grohne
2012-10-22finally parameterize CheckInsertHelmut Grohne
2012-09-26use _\==n_ and _\notin_ instead of \negHelmut Grohne
2012-09-26import [_] instead of Reveal_is_Helmut Grohne
2012-09-18one more application of lemma-just\==nnothingHelmut Grohne
2012-06-05move checkInsert and related properties to CheckInsert.agdaHelmut Grohne
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-01 20:31:37 +0000