summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-11-22shorten line length of theorem-1Helmut Grohne
2012-11-19turn lemma-fmap-just parameter into implicitHelmut Grohne
2012-11-19we can also drop an implicit parameter from assoc-enoughHelmut Grohne
2012-11-19we can use one more \exists in assoc-enoughHelmut Grohne
2012-11-19strip prose from assoc-enoughHelmut Grohne
2012-11-17strip prose from lemma-1 and lemma-2Helmut Grohne
2012-11-02rewrite checkInsert using "... |" notationHelmut Grohne
2012-10-25similarly rename lemma-from-map-just to map-just-injectiveHelmut Grohne
2012-10-25rename lemma-from-just to just-injectiveHelmut Grohne
2012-10-22Merge branch 'modparam'Helmut Grohne
2012-10-22finally parameterize CheckInsertHelmut Grohne
2012-10-22now parameterize BFFHelmut Grohne
2012-10-22also parameterize PrecondHelmut Grohne
2012-10-22parameterize Bidir via Carrier and deqHelmut Grohne
2012-10-05move all postulates to one moduleHelmut Grohne
2012-10-05remove VecRevBFFHelmut Grohne
2012-09-27remove getVec-getlen in favour of plain substHelmut Grohne
2012-09-27move definition of get-type to BFF and use it everywhereHelmut Grohne
2012-09-26use _\==n_ and _\notin_ instead of \negHelmut Grohne
2012-09-26rename suc-\== to suc-injectiveHelmut Grohne
2012-09-26import [_] instead of Reveal_is_Helmut Grohne
2012-09-18Merge branch 'using-vec'Helmut Grohne
2012-09-18one more application of lemma-just\==nnothingHelmut Grohne
2012-09-17save a with in lemma-\inn-lookupM-assocHelmut Grohne
2012-09-14employ rewrite in lemma-map-lookupM-assocHelmut Grohne
2012-09-14\::-subst is a special case of subst-congHelmut Grohne
2012-09-14vec-len-via-list and length-toList are the sameHelmut Grohne
2012-09-14complete missing parts of LiftGetHelmut Grohne
2012-09-11show fromList-toList in the subst formHelmut Grohne
2012-09-11LiftGet: replace vec-length-same with toList-substHelmut Grohne
2012-09-10LiftGet: vec-length is also known as subst (Vec A)Helmut Grohne
2012-09-08give a sufficient precondition for theorem-2Helmut Grohne
2012-09-04rewrite main theorems to using Vec instead of ListHelmut Grohne
2012-09-04formulate List <-> Vec isomorphism problemsHelmut Grohne
2012-08-30prove LiftGet.get-trafo-2-getlenHelmut Grohne
2012-08-30phrase other half of bijection in LiftGetHelmut Grohne
2012-08-30prove half of the bijection in LiftGetHelmut Grohne
2012-08-30give the type of different gets a nameHelmut Grohne
2012-08-06attempt isomorphism between get on List and on VecHelmut Grohne
2012-06-19third definition of bffHelmut Grohne
2012-06-05make the Vec bff more similar to the List versionHelmut Grohne
2012-06-05define a bff over VecHelmut Grohne
2012-06-05move bff and friends to submodule ListBFFHelmut Grohne
2012-06-05move checkInsert and related properties to CheckInsert.agdaHelmut Grohne
2012-04-27lemma-2: do not confuse lookup with lookupMHelmut Grohne
2012-04-27use fromFunc to define unionHelmut Grohne
2012-04-27prove the theorem-2Helmut Grohne
2012-04-20remove lemma-\in-lookupM-assocHelmut Grohne
2012-04-20complete lemma-2 using new property _in-domain-of_Helmut Grohne
2012-04-19reduce hole in lemma-2Helmut Grohne
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-01 20:31:00 +0000