projects / ~helmut / bidiragda.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
~helmut/bidiragda.git
2022-08-18 Helmut Grohnefix deprecation warning about Any.any with agda-stdlib... master commit | commitdiff | tree | snapshot
2020-08-01 Helmut Grohnemove imports for agda-stdlib 1.3 commit | commitdiff | tree | snapshot
2020-08-01 Helmut Grohneindividually open ≡-Reasoning commit | commitdiff | tree | snapshot
2019-09-29 Helmut Grohneport to agda/2.6.0.1 and agda-stdlib/1.1 commit | commitdiff | tree | snapshot
2019-03-31 Helmut GrohneGeneric.toList-fromList is Data.Vec.Properties.toList... commit | commitdiff | tree | snapshot
2019-03-31 Helmut GrohneGeneric.just-injective is Data.Maybe.just-injective commit | commitdiff | tree | snapshot
2019-03-31 Helmut GrohneFinMap.lemma-lookupM-delete is another variant of Data... commit | commitdiff | tree | snapshot
2019-03-31 Helmut GrohneFinMap.lemma-lookupM-fromFunc is almost Data.Vec.Proper... commit | commitdiff | tree | snapshot
2019-03-31 Helmut GrohneFinMap.lemma-tabulate-∘ is also known as Data.Vec.Prope... commit | commitdiff | tree | snapshot
2019-03-31 Helmut Grohnereplace FinMap.lemma-lookupM-empty with Data.Vec.Proper... commit | commitdiff | tree | snapshot
2018-11-25 Helmut Grohneport to agda/2.5.4.1 and agda-stdlib/0.17 commit | commitdiff | tree | snapshot
2018-11-25 Helmut Grohneremove unused imports commit | commitdiff | tree | snapshot
2018-11-25 Helmut Grohnemake the setoid parameter to sequenceV-cong explicit commit | commitdiff | tree | snapshot
2018-11-25 Helmut Grohnereorganize equality imports commit | commitdiff | tree | snapshot
2018-11-25 Helmut Grohnefix missing import of "length" commit | commitdiff | tree | snapshot
2018-01-02 Helmut Grohnelength-replicate is now upstream as well commit | commitdiff | tree | snapshot
2018-01-02 Helmut Grohneremove lemma-lookupM-insert-other in favour of lookup... commit | commitdiff | tree | snapshot
2018-01-02 Helmut Grohneremove lemma-lookupM-insert in favour of lookup∘update commit | commitdiff | tree | snapshot
2018-01-01 Helmut Grohnefix compilation with agda 2.5.3, agda-stdlib 0.14 commit | commitdiff | tree | snapshot
2016-06-21 Helmut Grohnefix compilation with agda 2.5.1, agda-stdlib 0.12 commit | commitdiff | tree | snapshot
2015-08-11 Helmut Grohnedeclare copyright and license commit | commitdiff | tree | snapshot
2015-07-02 Helmut Grohnesplit lemma-union-not-used into lemma-exchange-maps commit | commitdiff | tree | snapshot
2015-06-12 Helmut Grohneadd example applications of bff commit | commitdiff | tree | snapshot
2015-06-10 Helmut Grohneuse "module _" to simplify types involving Get records commit | commitdiff | tree | snapshot
2015-06-09 Helmut Grohnedrop barred members from GetTypes commit | commitdiff | tree | snapshot
2015-06-09 Helmut Grohnedrop the Function.Equality requirement from GetTypes commit | commitdiff | tree | snapshot
2015-06-03 Helmut Grohnerewrite lemma-disjoint-union in a more compositional way commit | commitdiff | tree | snapshot
2015-01-05 Helmut GrohneSetoidReasoning is no longer needed commit | commitdiff | tree | snapshot
2015-01-05 Helmut Grohneturns out: ind-cong is a special case of H.cong₂ commit | commitdiff | tree | snapshot
2014-11-26 Helmut Grohnefix compilation against agda stdlib 0.9 commit | commitdiff | tree | snapshot
2014-10-30 Helmut Grohnemake more parameters implicit commit | commitdiff | tree | snapshot
2014-10-21 Helmut Grohnemove all those toList calls inside _in-domain-of_ commit | commitdiff | tree | snapshot
2014-10-20 Helmut Grohnechange restrict and fromAscList to work with Vec commit | commitdiff | tree | snapshot
2014-10-17 Helmut Grohnegeneralize lemma-union-not-used commit | commitdiff | tree | snapshot
2014-10-16 Helmut Grohnesym result of lemma-lookupM-{i,checkI}nsert-other commit | commitdiff | tree | snapshot
2014-10-15 Helmut Grohneremove lemma-just≢nothing commit | commitdiff | tree | snapshot
2014-10-14 Helmut Grohnedrop the injection requirement for gl₁ commit | commitdiff | tree | snapshot
2014-09-26 Helmut Grohneresolve ambiguity in BFFPlug commit | commitdiff | tree | snapshot
2014-06-06 Helmut Grohnedrop-suc is cong pred commit | commitdiff | tree | snapshot
2014-04-03 Helmut Grohnefix compilation for Agda 2.3.0.1 again commit | commitdiff | tree | snapshot
2014-04-03 Helmut GrohneMerge branch feature-shaped into master commit | commitdiff | tree | snapshot
2014-04-03 Helmut Grohnedrop PartialShapeVec commit | commitdiff | tree | snapshot
2014-03-10 Helmut Grohnealso allow Shaped types for the view commit | commitdiff | tree | snapshot
2014-03-10 Helmut Grohnegeneralize lemma-{just-sequence,sequence-successful} commit | commitdiff | tree | snapshot
2014-03-10 Helmut GrohneExample: show that PairVec is Shaped commit | commitdiff | tree | snapshot
2014-03-10 Helmut Grohneport precondition to PartialShapeVec commit | commitdiff | tree | snapshot
2014-03-10 Helmut Grohneport theorem-{1,2} to PartialShapeVec commit | commitdiff | tree | snapshot
2014-03-10 Helmut Grohneimplement a bff on a shaped source type commit | commitdiff | tree | snapshot
2014-03-07 Helmut Grohneadd a Functor structure commit | commitdiff | tree | snapshot
2014-03-07 Helmut Grohneimprove notation of theorem-1 using local bindings commit | commitdiff | tree | snapshot
2014-03-07 Helmut Grohneuse allFin rather than tabulate id commit | commitdiff | tree | snapshot
2014-03-05 Helmut GrohneMerge branch feature-omit-sequence into master commit | commitdiff | tree | snapshot
2014-03-04 Helmut Grohnemake lemma-sequenceV-successful more precise commit | commitdiff | tree | snapshot
2014-02-26 Helmut Grohneweaken assumptions made by theorem-2 and asssoc-enough commit | commitdiff | tree | snapshot
2014-02-26 Helmut Grohneremove the sequenceV call from bff commit | commitdiff | tree | snapshot
2014-02-26 Helmut Grohnefix compilation on Agda 2.3.0.1 commit | commitdiff | tree | snapshot
2014-02-26 Helmut Grohneconvert LiftGet module to using heterogeneous equality commit | commitdiff | tree | snapshot
2014-02-24 Helmut Grohneadd intersperse as another example commit | commitdiff | tree | snapshot
2014-02-24 Helmut Grohnetheorem-2 works with EqR rather than SetoidReasoning... commit | commitdiff | tree | snapshot
2014-02-24 Helmut Grohnedefine fromFunc more conveniently commit | commitdiff | tree | snapshot
2014-02-24 Helmut Grohnegeneralize/weaken lemma-get-mapMV commit | commitdiff | tree | snapshot
2014-02-24 Helmut Grohnedefine mapMV via sequenceV commit | commitdiff | tree | snapshot
2014-02-24 Helmut Grohnegeneralize lemma-lookupM-assoc commit | commitdiff | tree | snapshot
2014-02-21 Helmut Grohneminor simplifications commit | commitdiff | tree | snapshot
2014-02-21 Helmut Grohneuse map-Σ to simplify lemma-mapM-successful commit | commitdiff | tree | snapshot
2014-02-17 Helmut Grohnefix compilation on Agda 2.3.0.1 commit | commitdiff | tree | snapshot
2014-02-17 Helmut Grohneuse drop, tail and take from Data.Vec in examples commit | commitdiff | tree | snapshot
2014-02-17 Helmut Grohneswitch examples to PartialVecVec commit | commitdiff | tree | snapshot
2014-02-17 Helmut GrohneMerge branch feature-partial-getlen into master commit | commitdiff | tree | snapshot
2014-02-17 Helmut Grohneavoid useless repetition commit | commitdiff | tree | snapshot
2014-02-14 Helmut GrohneMerge branch feature-shape-update into master commit | commitdiff | tree | snapshot
2014-02-14 Helmut Grohneadd back original bff function before shape updates commit | commitdiff | tree | snapshot
2014-02-10 Helmut Grohneadd bffplug and bffinv functions and examples commit | commitdiff | tree | snapshot
2014-02-10 Helmut GrohneMerge branch master into feature-shape-update commit | commitdiff | tree | snapshot
2014-02-10 Helmut Grohneadd sieve to examples commit | commitdiff | tree | snapshot
2014-02-07 Helmut Grohneeliminate useless withs commit | commitdiff | tree | snapshot
2014-02-07 Helmut Grohnereplace rewrite with cong where feasible commit | commitdiff | tree | snapshot
2014-02-07 Helmut Grohneallow shape shape updates in bff commit | commitdiff | tree | snapshot
2014-02-05 Helmut Grohnebe more precise about which lookups we use commit | commitdiff | tree | snapshot
2014-02-05 Helmut Grohnestrip even more implementation detail in Precond commit | commitdiff | tree | snapshot
2014-02-05 Helmut Grohnestrip implementation detail from lemma-union-delete... commit | commitdiff | tree | snapshot
2014-02-05 Helmut Grohneadd lemma-lookupM-fromFunc commit | commitdiff | tree | snapshot
2014-02-05 Helmut Grohneadd examples commit | commitdiff | tree | snapshot
2014-02-04 Helmut Grohneremove unused imports commit | commitdiff | tree | snapshot
2014-02-04 Helmut Grohneadd convenience members to PartialVecVec.Get commit | commitdiff | tree | snapshot
2014-02-04 Helmut GrohneMerge branch feature-get-record into feature-partial... commit | commitdiff | tree | snapshot
2014-02-03 Helmut Grohnemake things compile with 2.3.0.1 commit | commitdiff | tree | snapshot
2014-02-03 Helmut GrohneMerge branch feature-get-record into master commit | commitdiff | tree | snapshot
2014-02-03 Helmut Grohnealso show the other direction GetL-to-GetV commit | commitdiff | tree | snapshot
2014-02-03 Helmut Grohneadd a GetV-to-GetL transformer commit | commitdiff | tree | snapshot
2014-01-30 Helmut Grohnefully allow partial get functions commit | commitdiff | tree | snapshot
2014-01-30 Helmut Grohnemake the getlen functions explicit in PartialVecBFF commit | commitdiff | tree | snapshot
2014-01-30 Helmut Grohneexpress VecBFF via PartialVecBFF commit | commitdiff | tree | snapshot
2014-01-30 Helmut Grohneallow importing of Bidir without any postulates commit | commitdiff | tree | snapshot
2014-01-30 Helmut Grohnepass get functions as records commit | commitdiff | tree | snapshot
2014-01-30 Helmut Grohnesimplify compilation of the whole source commit | commitdiff | tree | snapshot
2014-01-28 Helmut Grohnedefine bff on a partial getlen commit | commitdiff | tree | snapshot
2014-01-28 Helmut Grohneimprove readability using _∋_≈_ instead of Setoid._≈_ commit | commitdiff | tree | snapshot
2014-01-28 Helmut Grohnethere is no need to work with IsPreorder commit | commitdiff | tree | snapshot
2014-01-28 Helmut Grohneuse the indexed version of the Vec Setoid commit | commitdiff | tree | snapshot
next
Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)