| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-01-08 | Avoiding introducing yet another convention in naming files. | Hugo Herbelin | |
| 2013-12-04 | Derive plugin. | Arnaud Spiwack | |
| 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). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |