summaryrefslogtreecommitdiff
path: root/Precond.agda
AgeCommit message (Expand)Author
2019-03-31replace FinMap.lemma-lookupM-empty with Data.Vec.Properties.lookup-replicateHelmut Grohne
2018-11-25port to agda/2.5.4.1 and agda-stdlib/0.17Helmut Grohne
2018-11-25reorganize equality importsHelmut Grohne
2018-01-01fix compilation with agda 2.5.3, agda-stdlib 0.14Helmut Grohne
2015-06-10use "module _" to simplify types involving Get recordsHelmut Grohne
2015-06-09drop barred members from GetTypesHelmut Grohne
2014-11-26fix compilation against agda stdlib 0.9Helmut Grohne
2014-10-30make more parameters implicitHelmut Grohne
2014-10-21move all those toList calls inside _in-domain-of_Helmut Grohne
2014-10-16sym result of lemma-lookupM-{i,checkI}nsert-otherHelmut Grohne
2014-03-10also allow Shaped types for the viewHelmut Grohne
2014-03-10port precondition to PartialShapeVecHelmut Grohne
2014-03-07use allFin rather than tabulate idHelmut Grohne
2014-02-26weaken assumptions made by theorem-2 and asssoc-enoughHelmut Grohne
2014-02-26remove the sequenceV call from bffHelmut Grohne
2014-02-24define fromFunc more convenientlyHelmut Grohne
2014-02-24define mapMV via sequenceVHelmut Grohne
2014-02-17Merge branch feature-partial-getlen into masterHelmut Grohne
2014-02-07allow shape shape updates in bffHelmut Grohne
2014-02-05be more precise about which lookups we useHelmut Grohne
2014-02-05strip even more implementation detail in PrecondHelmut Grohne
2014-02-05strip implementation detail from lemma-union-delete-fromFuncHelmut Grohne
2014-02-04remove unused importsHelmut Grohne
2014-02-04add convenience members to PartialVecVec.GetHelmut Grohne
2014-02-04Merge branch feature-get-record into feature-partial-getlenHelmut Grohne
2014-02-03make things compile with 2.3.0.1Helmut Grohne
2014-01-30fully allow partial get functionsHelmut Grohne
2014-01-30allow importing of Bidir without any postulatesHelmut Grohne
2014-01-30pass get functions as recordsHelmut Grohne
2014-01-27Merge branch feature-deleteHelmut Grohne
2014-01-27cleanup unused functions and useless stepsHelmut Grohne
2014-01-27prove assoc-enough in the presence of deleteHelmut Grohne
2014-01-23generalize BFF and theorem-2 to arbitrary SetoidsHelmut Grohne
2014-01-17generalize checkInsert to arbitrary SetoidsHelmut Grohne
2013-12-17refactor to get rid of FinMap without Maybe entirelyHelmut Grohne
2013-12-17update bff implementation to use deleteHelmut 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
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-01 17:53:16 +0000