TypingBase
Raised in case of type error, not propagated because replaced by an error constructor in the proof
Raised in case of subtyping error, not propagated because replaced by an error constructor in the proof
exception Loop_error of Pos.popt
Raised when the termination checkers fails, propagated
val loop_error : Pos.popt -> 'a
type ctxt = {
sub_ihs : Ast.schema list; |
fix_ihs : fix_induction list; |
fix_todo : (unit -> unit) list Stdlib.ref; |
top_induction : induction_node; |
call_graphs : Sct.t; |
non_zero : Ast.ordi list; |
}
and fix_induction = (Ast.term', Ast.term) Bindlib.binder * Ast.schema list Stdlib.ref
induction hypothesis for typing recursive programs
val empty_ctxt : unit -> ctxt
the initial empty context
val run_fix_todo : ctxt -> unit
run the registered functions.
val consecutive : (int * Ast.ordi) list -> bool
val opred : Ast.ordi -> Ast.ord_wit -> Ast.ordi
construction of an ordinal < o such that w
val print_nz : 'a -> ctxt -> unit
val has_leading_ord_quantifier : Ast.kind -> bool
val has_leading_exists : Ast.kind -> bool
val has_leading_forall : Ast.kind -> bool
val has_uvar : Ast.kind -> bool