blob: 3fee1f777d85d07b542870cdfee2f33fa0bad0d3 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
|
(* Extraction driver: turns the proven checker of
theories/DecreaseChecker.v into lib/decrease_extracted.ml, which
Pattern.strictly_contains runs. Kept beside the library so the
generated module lands where dune collects it. *)
From Stdlib Require Import Extraction ExtrOcamlBasic ExtrOcamlNatInt.
Require Import DecreaseChecker.
Require Import Lex.
Extraction "decrease_extracted.ml" contains term_eqb lex_ltb.
|
