diff options
Diffstat (limited to '')
| -rw-r--r-- | lib/pattern.mli | 11 |
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 |