| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
Instead of forcing the specifying property to be of the form (r spec def), allow any lemma depending on def.
|
| | |
|
| |
|
|
| |
stdlib does not compile entirely).
|
| |
|
| |
My bad, I forgot to fix the classification before comitting.
|
|
|
A small plugin to support program deriving (à la Richard Bird) in Coq.
It's fairly simple:
Require Coq.Derive.Derive.
Derive f From g Upto eq As h.
Produces a goal (actually two, but the first one is automatically shelved):
|- eq g ?42
And closing the proof produces two definitions: f is instantiated with the value of ?42 (it's always transparent). And h is instantiated with the content of the proof (it is transparent or opaque depending on whether the proof was closed with Defined or Qed).
|
Arnaud Spiwack
Enrico Tassi
Matthieu Sozeau