path: root/lib/extract.v

(* 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.