coq/plugins/Derive/vo.itarget, branch master The formal proof system Avoiding introducing yet another convention in naming files. 2015-01-08T18:05:14+00:00 Hugo Herbelin 2015-01-08T17:18:02+00:00 d08532d5344d96d10604760fa44109c9d56e73ce 






Derive plugin.
2013-12-04T13:14:33+00:00

Arnaud Spiwack

2013-11-25T18:05:48+00:00

078efbe2dfff0b783cd35b0b3ab2354f554e95a6

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).





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).