Typingtype ind = | Use of Ast.schema | (* The given induction hypothesis applies. *) |
| New of (Ast.schema * Ast.kind * Ast.kind * (Ast.ordi * Ast.ordi) list) option | (* The given induction hypothesis has been registered. *) |
Result type of check_rec.
val check_rec : TypingBase.ctxt -> Ast.term -> Ast.kind -> Ast.kind -> ind * TypingBase.ctxtcheck_rec ctxt t a b checks whether a given pointed subtyping relation can be derived in the current context using an induction hypothesis. If not, the current schema is registered as an induction hypothesis so that it can be used in a later call to check_rec.
val search_induction : (TypingBase.ctxt -> 'a -> Ast.kind -> Ast.kind -> Ast.sub_prf) -> Ast.typ_gen Stdlib.ref -> TypingBase.ctxt -> 'a -> Ast.kind -> Ast.schema list -> unitval check_fix : (TypingBase.ctxt -> Ast.term -> Ast.kind -> Ast.typ_prf) -> (TypingBase.ctxt -> 'a -> Ast.kind -> Ast.kind -> Ast.sub_prf) -> Ast.typ_gen Stdlib.ref -> TypingBase.ctxt -> 'a -> bool option -> int -> (Ast.term', Ast.term) Bindlib.binder -> Ast.kind -> unitval is_subtype : TypingBase.ctxt -> Ast.term -> Ast.kind -> Ast.kind -> boolA boolean test for subtyping
val subtype : Ast.term option -> Ast.kind -> Ast.kind -> Ast.sub_prf * Sct.tsubtype t a b checks the pointed subtyping relation "t ∈ A ⊂ B". Since the term t is optional, a generic witness is used when t = None. The function returns a subtyping proof together with the successful instance of the SCT.
val type_check : Ast.term -> Ast.kind option -> Ast.kind * Ast.typ_prf * Sct.ttype_check t ko type-checks the term t against the optional type k (or a unification variable). The function returns a type for t and the corresponding typing proof and successful instance of the SCT. When the function is called with ko = Some k, the returned type is k.