Automate fixpoint proofs until alpha_FVars

jvanbruegge · Oct 29, 2024 · d2413b7 · d2413b7
1 parent 6df6526
commit d2413b7
Show file tree

Hide file tree

Showing 6 changed files with 851 additions and 374 deletions.
diff --git a/Tools/binder_inductive.ML b/Tools/binder_inductive.ML
@@ -13,8 +13,6 @@ fun long_name ctxt name =
     Const (s, _) => s
   | _ => error ("Undeclared constant: " ^ quote name)
 
-datatype ('a, 'b) either = Inl of 'a | Inr of 'b
-
 fun collapse (Inl x) = x
   | collapse (Inr x) = x
 

diff --git a/Tools/mrbnf_fp.ML b/Tools/mrbnf_fp.ML
diff --git a/Tools/mrbnf_util.ML b/Tools/mrbnf_util.ML
@@ -2,6 +2,8 @@ signature MRBNF_UTIL =
 sig
   include BNF_UTIL
 
+  datatype ('a, 'b) either = Inl of 'a | Inr of 'b
+
   val filter_like: 'a list -> ('a -> bool) -> 'b list -> 'b list
   val cond_keep: 'a list -> bool list -> 'a list
   val cond_interlace: 'a list -> 'a list -> bool list -> 'a list
@@ -71,6 +73,8 @@ struct
 
 open BNF_Util
 
+datatype ('a, 'b) either = Inl of 'a | Inr of 'b
+
 fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) = apfst (cons (x, T)) (strip_ex t)
   | strip_ex t = ([], t)