lexicographic order proven well founded, checker extracted and verifying admission

1 files changed, 11 insertions, 0 deletions

diff --git a/lib/pattern.mli b/lib/pattern.mli
index 5fc16c6..f79dce0 100644
--- a/lib/pattern.mli
+++ b/lib/pattern.mli
@@ -45,6 +45,17 @@ val strictly_contains : t -> sub:t -> bool
 
 val pp : Format.formatter -> t -> unit
 
+(** The verified checker's view of patterns. Admission projects
+    patterns through {!to_checker} and runs the containment and
+    lexicographic checkers extracted from Rocq; the conversion is
+    injective by leaf kind, and these two equalities are the
+    trusted seam. *)
+type checker_leaf
+
+val checker_leaf_equal : checker_leaf -> checker_leaf -> bool
+
+val to_checker : t -> (Label.t, checker_leaf) Decrease_extracted.term
+
 (** Substitutions bind variables to patterns. They only grow;
     unification never revokes a binding. *)
 module Subst : sig