Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Avoiding introducing yet another convention in naming files. | 2015-01-08 | |
| | |||
* | Derive plugin. | 2013-12-04 | |
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). |