val infer_exn : Ctx.t -> untyped -> LogtkType.t * typed Closure.tInfer the type of this term under the given signature. This updates the context's typing environment!
the context
the untyped term whose type must be inferred
the inferred type of the untyped term (possibly a type var) along with a closure to produce a typed term once every constraint has been solved
LogtkType.Error if the types are inconsistent
Safe version of infer_exn. It returns `Error s rather than raising LogtkType.Error if the typechecking fails.
This section is mostly useful for inferring a signature without converting untyped_terms into typed_terms.
Force the two terms to have the same type in this context
LogtkType.Error if an inconsistency is detected
val constrain_term_type_exn : Ctx.t -> untyped -> LogtkType.t -> unitForce the term's type and the given type to be the same.
LogtkType.Error if an inconsistency is detected
Safe version of constrain_term_term_exn
val constrain_term_type : Ctx.t -> untyped -> LogtkType.t -> unit or_errorSafe version of constrain_term_type_exn