fix compilation with agda 2.5.3, agda-stdlib 0.14
[~helmut/bidiragda.git] / Precond.agda
2018-01-01 Helmut Grohnefix compilation with agda 2.5.3, agda-stdlib 0.14
2015-06-10 Helmut Grohneuse "module _" to simplify types involving Get records
2015-06-09 Helmut Grohnedrop barred members from GetTypes
2014-11-26 Helmut Grohnefix compilation against agda stdlib 0.9
2014-10-30 Helmut Grohnemake more parameters implicit
2014-10-21 Helmut Grohnemove all those toList calls inside _in-domain-of_
2014-10-16 Helmut Grohnesym result of lemma-lookupM-{i,checkI}nsert-other
2014-04-03 Helmut GrohneMerge branch feature-shaped into master
2014-03-10 Helmut Grohnealso allow Shaped types for the view
2014-03-10 Helmut Grohneport precondition to PartialShapeVec
2014-03-07 Helmut Grohneuse allFin rather than tabulate id
2014-03-05 Helmut GrohneMerge branch feature-omit-sequence into master
2014-02-26 Helmut Grohneweaken assumptions made by theorem-2 and asssoc-enough
2014-02-26 Helmut Grohneremove the sequenceV call from bff
2014-02-24 Helmut Grohnedefine fromFunc more conveniently
2014-02-24 Helmut Grohnedefine mapMV via sequenceV
2014-02-17 Helmut GrohneMerge branch feature-partial-getlen into master
2014-02-14 Helmut GrohneMerge branch feature-shape-update into master
2014-02-10 Helmut GrohneMerge branch master into feature-shape-update
2014-02-07 Helmut Grohneallow shape shape updates in bff
2014-02-05 Helmut Grohnebe more precise about which lookups we use
2014-02-05 Helmut Grohnestrip even more implementation detail in Precond
2014-02-05 Helmut Grohnestrip implementation detail from lemma-union-delete...
2014-02-04 Helmut Grohneremove unused imports
2014-02-04 Helmut Grohneadd convenience members to PartialVecVec.Get
2014-02-04 Helmut GrohneMerge branch feature-get-record into feature-partial...
2014-02-03 Helmut Grohnemake things compile with
2014-02-03 Helmut GrohneMerge branch feature-get-record into master
2014-01-30 Helmut Grohnefully allow partial get functions
2014-01-30 Helmut Grohneallow importing of Bidir without any postulates
2014-01-30 Helmut Grohnepass get functions as records
2014-01-27 Helmut GrohneMerge branch feature-delete
2014-01-27 Helmut GrohneMerge branch feature-decsetoid
2014-01-27 Helmut Grohnecleanup unused functions and useless steps
2014-01-27 Helmut Grohneprove assoc-enough in the presence of delete
2014-01-23 Helmut Grohnegeneralize BFF and theorem-2 to arbitrary Setoids
2014-01-17 Helmut Grohnegeneralize checkInsert to arbitrary Setoids
2013-12-17 Helmut Grohnerefactor to get rid of FinMap without Maybe entirely
2013-12-17 Helmut Grohneupdate bff implementation to use delete
2013-07-21 Helmut Grohneimport _>>=_ and fmap from Data.Maybe
2013-04-19 Helmut Grohnemove lemma-\notin-lookupM-assoc to Precond
2013-04-14 Helmut Grohnesimpler formulation of All-different
2013-01-10 Helmut Grohneclean imports of Precond
2013-01-10 Helmut Grohneuse different formulation of all-different
2012-12-14 Helmut Grohneun-inline different-drop
2012-11-19 Helmut Grohnewe can also drop an implicit parameter from assoc-enough
2012-11-19 Helmut Grohnewe can use one more \exists in assoc-enough
2012-11-19 Helmut Grohnestrip prose from assoc-enough
2012-10-22 Helmut GrohneMerge branch 'modparam'
2012-10-22 Helmut Grohnefinally parameterize CheckInsert
2012-10-22 Helmut Grohnenow parameterize BFF
2012-10-22 Helmut Grohnealso parameterize Precond
2012-09-27 Helmut Grohnemove definition of get-type to BFF and use it everywhere
2012-09-26 Helmut Grohnerename suc-\== to suc-injective
2012-09-18 Helmut GrohneMerge branch 'using-vec'
2012-09-08 Helmut Grohnegive a sufficient precondition for theorem-2