Derive plugin.

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

1 files changed, 1 insertions, 0 deletions

diff --git a/plugins/Derive/Derive.v b/plugins/Derive/Derive.v
new file mode 100644
index 0000000000..0d5a93b034
--- /dev/null
+++ b/plugins/Derive/Derive.v
@@ -0,0 +1 @@
+Declare ML Module "derive_plugin".
\ No newline at end of file