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