| Age | Commit message (Collapse) | Author |
|---|
|
* Data.Vec.lookup changed parameter order.
* A number of symbols were moved from Data.Maybe to submodules.
* In a number of occasions, agda no longer figures implicit arguments
and they had to be made explicit.
* We can no longer use heterogeneous proofs inside equational reasoning
for propositional equality. Use heterogeneous equational reasoning.
* Stop importing proof-irrelevance as that would require K.
|
|
|
|
|
|
|
|
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.
|
|
Broken in parent commit.
|
|
|
|
This makes a few proofs easier and eliminates the need for sequence-map
entirely.
|
|
It allows defining get functions that are only defined for some vector
lengths. It retains backwards compatibility with the previous state via
a VecVec compatibility module. The biggest benefit is that now standard
library functions such as tail, take and drop can be passed to bff.
Conflicts: heavy
BFF.agda (imports, bff type clash)
Bidir.agda (imports, heavy bff type clash in theorem-{1,2} and
lemma-get-mapMV)
Generic.agda (imports)
Precond.agda (imports, bff type clash in assoc-enough)
|
|
|
|
|
|
* Remove let patter , match = foo usage
* Remove Qualified.infix-symbol usage
* Add non-obvious absurd patterns
* Qualify constructors
|
|
|
|
|
|
|
|
Most conflicts stem from varying imports or added functions and a
take-both approach merges them. A notable exception is theorem-2, where
a new result sequence-cong was required. Apart from that, theorem-2
could be taken almost verbatim from feature-delete albeit its type
coming from feature-decsetoid.
Conflicts:
Bidir.agda
FinMap.agda
Generic.agda
Precond.agda
|
|
|
|
The biggest piece of this puzzle was establishing
get <$> mapMV f v == mapMV f (get v)
provided that the result of mapMV is just something.
lemma-union-not-used lost a "map just", but could be retained in
structure.
|
|
We get the plain Setoid for free then.
|
|
The general idea is to enable bff to use arbitrary DecSetoids.
* assoc needs to learn about DecSetoid
* checkInsert needs to learn about DecSetoid
* InsertionResult needs to learn about Setoid
* Parameters to InsertionResult.same become weaker
* lemma-checkInsert-restrict should work with weaker same
* lemma-insert-same needs to learn about Setoid
|
|
|
|
|
