From 078efbe2dfff0b783cd35b0b3ab2354f554e95a6 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Mon, 25 Nov 2013 19:05:48 +0100 Subject: Derive plugin. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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). --- plugins/pluginsbyte.itarget | 1 + 1 file changed, 1 insertion(+) (limited to 'plugins/pluginsbyte.itarget') diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget index 8f68cc696..744b07539 100644 --- a/plugins/pluginsbyte.itarget +++ b/plugins/pluginsbyte.itarget @@ -19,3 +19,4 @@ syntax/r_syntax_plugin.cma syntax/string_syntax_plugin.cma syntax/z_syntax_plugin.cma quote/quote_plugin.cma +Derive/derive_plugin.cma \ No newline at end of file -- cgit v1.2.3