From f22834d3aaed2b2dd2c5d4203e937fc8fb4b5507 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 22:03:21 -0300 Subject: admission runs the containment checker extracted from rocq --- lib/extract.v | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 lib/extract.v (limited to 'lib/extract.v') diff --git a/lib/extract.v b/lib/extract.v new file mode 100644 index 0000000..5c8ff7c --- /dev/null +++ b/lib/extract.v @@ -0,0 +1,9 @@ +(* 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. +Require Import DecreaseChecker. + +Extraction "decrease_extracted.ml" contains term_eqb. -- cgit v1.2.3