diff options
Diffstat (limited to '')
| -rw-r--r-- | proof/Extraction.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/proof/Extraction.v b/proof/Extraction.v new file mode 100644 index 0000000..dc93c21 --- /dev/null +++ b/proof/Extraction.v @@ -0,0 +1,17 @@ +(** * Extraction to OCaml — finiteness gate only + + Extracts [predicted_finite] to [lib/drl_verified/drl_verified.ml]. + To regenerate: cd proof && make *) + +From Stdlib Require Import Extraction. +From Stdlib Require Import ExtrOcamlBasic. +From Stdlib Require Import ExtrOcamlString. +From Stdlib Require Import ExtrOcamlNatInt. + +Require Import Schema. +Require Import Relation. +Require Import Drl. + +Set Extraction Output Directory "../lib/drl_verified". + +Extraction "drl_verified" predicted_finite. |