type_of_term term gamma
Compute the type of term
Precondition: term must be welltyped and the context valid.
val split_type :
Term.typ ->
Gamma.t ->
(Term.Pi_info.t * Term.typ) list * Term.typval split_kind :
Term.typ ->
Gamma.t ->
((Term.Pi_info.t * Term.typ) list * Term.Sort.t) optionsplit_kind k gamma:
Compute the arguments and the sort of the kind k. If typ does not reduce to a kind, then return None.
Precondition: k must be welltyped and the context gamma must be valid.
A kind has the form
all (x: A) (y: B) .... : swhere s is a sort.
val sort_of_kind : Term.typ -> Gamma.t -> Term.Sort.t optionsort_of_kind typ gamma
Compute the sort of the kind typ. If typ does not reduce to a kind, then return None.
Precondition: typ must be welltyped and the context gamma must be valid.
A kind has the form
all (x: A) (y: B) .... : swhere s is a sort.
is_kind typ gamma
Is the welltyped term typ in the valid context gamma a kind?
val key_split :
Term.t ->
Gamma.t ->
Term.t * (Term.t * Term.Application_info.t) listkeynormal term gamma
Compute the key normal form of the welltyped term term in the valid context gamma.
normalize_pi typ gamma
Precondition:
typ must be a valid type
Result: typ is expanded until the form
all (a: A) (b: B) ... : Ris reached where R cannot be expanded further into a product type.
normalize term gamma
Compute the normal form of the welltyped term term in the valid context gamma.
val check_naming_convention :
string ->
Term.typ ->
Gamma.t ->
(unit, name_violation) result