| 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.
|
|
These will happen to break with later agda-stdlib releases.
|
|
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.
|
|
|
|
|
|
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.
|
|
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.
|
|
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.
|
|
Special case of contradiction.
|
|
|
|
|
|
We can actually get semantic equality there without requiring anything
else. Indeed this was already hinted in the BX for free paper that says,
that lemma-1 holds in semantic equality.
|
|
This is another step towards permitting arbitrary Setoids in bff.
|
|
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
|
|
|
|
|
|
Get rid of checkInsertProof entirely.
Conflicts:
Bidir.agda (change of lemma-just\==nnothing
vs. checkInsertProof removal)
|
|
If one had a parameter of type just x \== nothing it could be simply
refuted by case splitting. So the cases where lemma-just\==nnothing was
used always employed trans to combine two results. The new version takes
both results instead.
|
|
Thanks to Joachim Breitner for helping me to work out the definition of
InsertionResult and to Daniel Seidel for helping me understand what
makes a view.
|
|
Now it looks a lot more like lemma-lookupM-insert-other, so rename it to
lemma-lookupM-checkInsert-other.
|
|
Suggested by Joachim Breitner.
|
|
|
|
|
|
Less characters => more readable.
|
|
We already have suc-injective and \::-injective. Consistency!
|
|
Also adapt depending modules. Long lines generally become shorter. The
misleading name "EqInst" (hiding the decidability) got discarded.
|
|
Consistent. Shorter.
|
|
This makes things a little shorter and more readable.
|
|
|
|
|
