| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
|
|
|
