lambdapi

Proof assistant for the λΠ-calculus modulo rewriting
Library lambdapi.core
Module Core . Infer
val infer_noexn : Term.problem -> Term.ctxt -> Term.term -> (Term.term * Term.term) option

infer_noexn p ctx t returns None if the type of t in context ctx cannot be inferred, or Some a where a is some type of t in the context ctx, possibly adding new constraints in p. The metavariables of p are updated when a metavariable is instantiated or created. ctx must be well sorted.

val check_noexn : Term.problem -> Term.ctxt -> Term.term -> Term.term -> Term.term option

check_noexn p ctx t a tells whether the term t has type a in the context ctx, possibly adding new constraints in p. The metavariables of p are updated when a metavariable is instantiated or created. The context ctx and the type a must be well sorted.

val check_sort_noexn : Term.problem -> Term.ctxt -> Term.term -> (Term.term * Term.term) option