summaryrefslogtreecommitdiff
path: root/Precond.agda
AgeCommit message (Expand)Author
2014-01-17generalize checkInsert to arbitrary SetoidsHelmut Grohne
2013-07-21import _>>=_ and fmap from Data.MaybeHelmut Grohne
2013-04-19move lemma-\notin-lookupM-assoc to PrecondHelmut Grohne
2013-04-14simpler formulation of All-differentHelmut Grohne
2013-01-10clean imports of PrecondHelmut Grohne
2013-01-10use different formulation of all-differentHelmut Grohne
2012-12-14un-inline different-dropHelmut 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-10-22finally parameterize CheckInsertHelmut Grohne
2012-10-22now parameterize BFFHelmut Grohne
2012-10-22also parameterize PrecondHelmut Grohne
2012-09-27move definition of get-type to BFF and use it everywhereHelmut Grohne
2012-09-26rename suc-\== to suc-injectiveHelmut Grohne
2012-09-08give a sufficient precondition for theorem-2Helmut Grohne
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-01 20:22:20 +0000