| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-03-31 | Generic.toList-fromList is Data.Vec.Properties.toList∘fromList | Helmut Grohne | |
| 2019-03-31 | Generic.just-injective is Data.Maybe.just-injective | Helmut Grohne | |
| 2019-03-31 | FinMap.lemma-lookupM-delete is another variant of ↵ | Helmut Grohne | |
| Data.Vec.Properties.lookup∘update′ | |||
| 2019-03-31 | FinMap.lemma-lookupM-fromFunc is almost Data.Vec.Properties.lookup∘tabulate | Helmut Grohne | |
| 2019-03-31 | FinMap.lemma-tabulate-∘ is also known as Data.Vec.Properties.tabulate-cong | Helmut Grohne | |
| 2019-03-31 | replace FinMap.lemma-lookupM-empty with Data.Vec.Properties.lookup-replicate | Helmut Grohne | |
| 2018-11-25 | port to agda/2.5.4.1 and agda-stdlib/0.17 | Helmut Grohne | |
| 2018-11-25 | remove unused imports | Helmut Grohne | |
| These will happen to break with later agda-stdlib releases. | |||
| 2018-11-25 | make the setoid parameter to sequenceV-cong explicit | Helmut Grohne | |
| Later versions of agda will be unable to infer it unambiguously. | |||
| 2018-11-25 | reorganize equality imports | Helmut Grohne | |
| Since we are working with multiple setoids now, it makes more sense to qualify their members. Follow the "as P" pattern from the standard library. Also stop importing those symbols from Relation.Binary.Core as later agda-stdlib versions will move them away. Rather than EqSetoid or PropEq, use P.setoid consistently. | |||
| 2018-11-25 | fix missing import of "length" | Helmut Grohne | |
| Broken in parent commit. | |||
| 2018-01-02 | length-replicate is now upstream as well | Helmut Grohne | |
| 2018-01-02 | remove lemma-lookupM-insert-other in favour of lookup∘update′ | Helmut Grohne | |
| 2018-01-02 | remove lemma-lookupM-insert in favour of lookup∘update | Helmut Grohne | |
| 2018-01-01 | fix compilation with agda 2.5.3, agda-stdlib 0.14 | Helmut Grohne | |
| 2016-06-21 | fix compilation with agda 2.5.1, agda-stdlib 0.12 | Helmut Grohne | |
| 2015-08-11 | declare copyright and license | Helmut Grohne | |
| 2015-07-02 | split lemma-union-not-used into lemma-exchange-maps | Helmut Grohne | |
| New type suggested by Janis Voigtländer. | |||
| 2015-06-12 | add example applications of bff | Helmut Grohne | |
| 2015-06-10 | use "module _" to simplify types involving Get records | Helmut Grohne | |
| 2015-06-09 | drop barred members from GetTypes | Helmut Grohne | |
| These became duplicates of their non-barred counterparts. | |||
| 2015-06-09 | drop the Function.Equality requirement from GetTypes | Helmut Grohne | |
| We never used the equality property. Thus a simple function is sufficient here. We always fulfilled the property using ≡-to-Π anyway. | |||
| 2015-06-03 | rewrite lemma-disjoint-union in a more compositional way | Helmut Grohne | |
| 2015-01-05 | SetoidReasoning is no longer needed | Helmut Grohne | |
| 2015-01-05 | turns out: ind-cong is a special case of H.cong₂ | Helmut Grohne | |
| The major differences between them are: * ind-cong treats the first parameter to the function implicit whereas H.cong₂ makes it explicit. * ind-cong expects a propositional proof for the first equality whereas H.cong₂ asks for a heterogeneous one. Lift using H.reflexive. | |||
| 2014-11-26 | fix compilation against agda stdlib 0.9 | Helmut Grohne | |
| 2014-10-30 | make more parameters implicit | Helmut Grohne | |
| All of these changes were applied to functions of type ... -> (x : ...) -> ... == x -> ... where x could be preceded by just making the x implicit, because it can be uniquely deduced from the equality proof. | |||
| 2014-10-21 | move all those toList calls inside _in-domain-of_ | Helmut Grohne | |
| 2014-10-20 | change restrict and fromAscList to work with Vec | Helmut Grohne | |
| While they do work with Lists and there is no inherent need to know the length, they are most often invoked in a context where a Vec needs to be converted to a List using toList. By changing them to work with Vec, quite a few toList calls can be dropped. | |||
| 2014-10-17 | generalize lemma-union-not-used | Helmut Grohne | |
| 2014-10-16 | sym result of lemma-lookupM-{i,checkI}nsert-other | Helmut Grohne | |
| Typically we have the complex term on the LHS and the simplified term on the RHS. These lemmata did it otherwise and by symming them, we save two syms. | |||
| 2014-10-15 | remove lemma-just≢nothing | Helmut Grohne | |
| Special case of contradiction. | |||
| 2014-10-14 | drop the injection requirement for gl₁ | Helmut Grohne | |
| Turns out, we never use this requirement. The only place where it may come in relevant is the free theorems. But here non-injectivity turns out to be reasoning about multiple get functions that are selected by the additional index each individually satisfying the free theorem and thus commonly satisfying it as well. | |||
| 2014-09-26 | resolve ambiguity in BFFPlug | Helmut Grohne | |
| Fixes compilation with Agda 2.4.2. | |||
| 2014-06-06 | drop-suc is cong pred | Helmut Grohne | |
| 2014-04-03 | fix compilation for Agda 2.3.0.1 again | Helmut Grohne | |
| It fails to infer the type of MaybeFunctor._<$>_, so give it explicitly. | |||
| 2014-04-03 | Merge branch feature-shaped into master | Helmut Grohne | |
| Generalizing both Vecs in the type of get to instances of Shaped. Thus allowing trees and other data structures to be used. | |||
| 2014-04-03 | drop PartialShapeVec | Helmut Grohne | |
| One can use PartialShapeShape instead, so there is limited utility for this type. It is not used directly and there also is no PartialVecShape. | |||
| 2014-03-10 | also allow Shaped types for the view | Helmut Grohne | |
| Albeit long, this commit is relatively boring. | |||
| 2014-03-10 | generalize lemma-{just-sequence,sequence-successful} | Helmut Grohne | |
| 2014-03-10 | Example: show that PairVec is Shaped | Helmut Grohne | |
| Example inspired in VoigtlaenderHMW13. Note that Vec (α × β) (length s) is not Shaped in this way since its real index is only a number. | |||
| 2014-03-10 | port precondition to PartialShapeVec | Helmut Grohne | |
| 2014-03-10 | port theorem-{1,2} to PartialShapeVec | Helmut Grohne | |
| 2014-03-10 | implement a bff on a shaped source type | Helmut Grohne | |
| Add IsShaped and Shaped records describing shapely types as in Jay95. Implement bff on Shaped and rewrite PartialVecVec to use the vector shape retaining all proofs on the vector implementation. | |||
| 2014-03-07 | add a Functor structure | Helmut Grohne | |
| The intent is to replace some uses of Vec with a structure that also happens to be a functor. RawFunctors from the standard library provide no laws though, so we define a Functor structure that adds the laws. As an additional law congruence is added, because * Other standard library structures in Algebra.Structures also require congruence. * Otherwise the identity law would have to reason about different identities. | |||
| 2014-03-07 | improve notation of theorem-1 using local bindings | Helmut Grohne | |
| 2014-03-07 | use allFin rather than tabulate id | Helmut Grohne | |
| 2014-03-05 | Merge branch feature-omit-sequence into master | Helmut Grohne | |
| Beyond allowing default values during shape updates, this branch simplifies working with shapes other than Vec. | |||
| 2014-03-04 | make lemma-sequenceV-successful more precise | Helmut Grohne | |
| 2014-02-26 | weaken assumptions made by theorem-2 and asssoc-enough | Helmut Grohne | |
 |
index : ~helmut/bidiragda.git | |
| Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf) | Helmut Grohne |
| summaryrefslogtreecommitdiff |