blob: dc93c214a54e5a90c872557f21b44eef61b11ba3 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
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.
|
