2018-01-02 Helmut Grohnelength-replicate is now upstream as well master
2018-01-02 Helmut Grohneremove lemma-lookupM-insert-other in favour of lookup...
2018-01-02 Helmut Grohneremove lemma-lookupM-insert in favour of lookup∘update
2018-01-01 Helmut Grohnefix compilation with agda 2.5.3, agda-stdlib 0.14
2016-06-21 Helmut Grohnefix compilation with agda 2.5.1, agda-stdlib 0.12
2015-08-11 Helmut Grohnedeclare copyright and license
2015-07-02 Helmut Grohnesplit lemma-union-not-used into lemma-exchange-maps
2015-06-12 Helmut Grohneadd example applications of bff
2015-06-10 Helmut Grohneuse "module _" to simplify types involving Get records
2015-06-09 Helmut Grohnedrop barred members from GetTypes
2015-06-09 Helmut Grohnedrop the Function.Equality requirement from GetTypes
2015-06-03 Helmut Grohnerewrite lemma-disjoint-union in a more compositional way
2015-01-05 Helmut GrohneSetoidReasoning is no longer needed
2015-01-05 Helmut Grohneturns out: ind-cong is a special case of H.cong₂
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-20 Helmut Grohnechange restrict and fromAscList to work with Vec
2014-10-17 Helmut Grohnegeneralize lemma-union-not-used
2014-10-16 Helmut Grohnesym result of lemma-lookupM-{i,checkI}nsert-other
2014-10-15 Helmut Grohneremove lemma-just≢nothing
2014-10-14 Helmut Grohnedrop the injection requirement for gl₁
2014-09-26 Helmut Grohneresolve ambiguity in BFFPlug
2014-06-06 Helmut Grohnedrop-suc is cong pred
2014-04-03 Helmut Grohnefix compilation for Agda again
2014-04-03 Helmut GrohneMerge branch feature-shaped into master
2014-04-03 Helmut Grohnedrop PartialShapeVec
2014-03-10 Helmut Grohnealso allow Shaped types for the view
2014-03-10 Helmut Grohnegeneralize lemma-{just-sequence,sequence-successful}
2014-03-10 Helmut GrohneExample: show that PairVec is Shaped
2014-03-10 Helmut Grohneport precondition to PartialShapeVec
2014-03-10 Helmut Grohneport theorem-{1,2} to PartialShapeVec
2014-03-10 Helmut Grohneimplement a bff on a shaped source type
2014-03-07 Helmut Grohneadd a Functor structure
2014-03-07 Helmut Grohneimprove notation of theorem-1 using local bindings
2014-03-07 Helmut Grohneuse allFin rather than tabulate id
2014-03-05 Helmut GrohneMerge branch feature-omit-sequence into master
2014-03-04 Helmut Grohnemake lemma-sequenceV-successful more precise
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-26 Helmut Grohnefix compilation on Agda
2014-02-26 Helmut Grohneconvert LiftGet module to using heterogeneous equality
2014-02-24 Helmut Grohneadd intersperse as another example
2014-02-24 Helmut Grohnetheorem-2 works with EqR rather than SetoidReasoning...
2014-02-24 Helmut Grohnedefine fromFunc more conveniently
2014-02-24 Helmut Grohnegeneralize/weaken lemma-get-mapMV
2014-02-24 Helmut Grohnedefine mapMV via sequenceV
2014-02-24 Helmut Grohnegeneralize lemma-lookupM-assoc
2014-02-21 Helmut Grohneminor simplifications
2014-02-21 Helmut Grohneuse map-Σ to simplify lemma-mapM-successful
2014-02-17 Helmut Grohnefix compilation on Agda
2014-02-17 Helmut Grohneuse drop, tail and take from Data.Vec in examples
2014-02-17 Helmut Grohneswitch examples to PartialVecVec
2014-02-17 Helmut GrohneMerge branch feature-partial-getlen into master
2014-02-17 Helmut Grohneavoid useless repetition
2014-02-14 Helmut GrohneMerge branch feature-shape-update into master
2014-02-14 Helmut Grohneadd back original bff function before shape updates
2014-02-10 Helmut Grohneadd bffplug and bffinv functions and examples
2014-02-10 Helmut GrohneMerge branch master into feature-shape-update
2014-02-10 Helmut Grohneadd sieve to examples
2014-02-07 Helmut Grohneeliminate useless withs
2014-02-07 Helmut Grohnereplace rewrite with cong where feasible
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-05 Helmut Grohneadd lemma-lookupM-fromFunc
2014-02-05 Helmut Grohneadd examples
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-02-03 Helmut Grohnealso show the other direction GetL-to-GetV
2014-02-03 Helmut Grohneadd a GetV-to-GetL transformer
2014-01-30 Helmut Grohnefully allow partial get functions
2014-01-30 Helmut Grohnemake the getlen functions explicit in PartialVecBFF
2014-01-30 Helmut Grohneexpress VecBFF via PartialVecBFF
2014-01-30 Helmut Grohneallow importing of Bidir without any postulates
2014-01-30 Helmut Grohnepass get functions as records
2014-01-30 Helmut Grohnesimplify compilation of the whole source
2014-01-28 Helmut Grohnedefine bff on a partial getlen
2014-01-28 Helmut Grohneimprove readability using _∋_≈_ instead of Setoid._≈_
2014-01-28 Helmut Grohnethere is no need to work with IsPreorder
2014-01-28 Helmut Grohneuse the indexed version of the Vec Setoid
2014-01-28 Helmut Grohnecleanup unused function and import
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-24 Helmut Grohneprove theorem-2 in the presence of delete
2014-01-23 Helmut Grohnegeneralize BFF and theorem-2 to arbitrary Setoids
2014-01-23 Helmut Grohneshow a stronger lemma-checkInsert-restrict
2014-01-17 Helmut Grohnegeneralize checkInsert to arbitrary Setoids
2014-01-17 Helmut Grohneshow that Vec is an indexed Setoid
2014-01-16 Helmut Grohnegeneralize lemma-insert-same 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-12-16 Helmut Grohneadd a mapM variant on the Maybe monad on Vecs
2013-12-16 Helmut Grohnemove generic functions to a new Generic module