| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
| |
This closes #146 and makes `make quick` faster.
The changes were generated by adding [Global Set Suggest Proof Using.]
to GlobalSettings.v, and then following [the instructions for a script I
wrote](https://github.com/JasonGross/coq-tools#proof-using-helper).
|
| |
|
|
| |
It's a version of [Interp] that works even when there are destructuring lets.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
Andres Erbsen
Jason Gross