| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
This will eventually make a number of proofs easier.
Unfortunately, the correctness lemmas for AddCoordinates and LadderStep
no longer work (because of different arities), and there's a proof in
Experiments/Ed25519 that I've admitted.
The correctness lemmas will be easy to re-add when we have a more
general version that handle arbitrary type shapes.
|
| |
|
|
| |
There was duplicate code in Reflection.Equality and Reflection.TypeInversion
|
| | |
|
| |
|
|
| |
Now we don't loop on [Unit = Unit] hypotheses, clearing them instead.
|
| | |
|
| | |
|
| |
|
|
| |
It's be nice if we could find a uniform way to do this for all flat_types which resolve to constructors...
|
| |
|
Jason Gross