Module TypeInference

module TypeInference: sig .. end

Scoping and Type Inference

type 'a or_error = ('a, string) CCResult.t

type id = Nunchaku_core.ID.t

type 'a var = 'a Nunchaku_core.Var.t

type loc = Nunchaku_core.Location.t

exception ScopingError of string * string * loc option

Scoping error for the given variable

Functions exposed by this functor will mutate in place their input, by calling Term.Ty.bind.

type attempt_stack = Nunchaku_core.UntypedAST.term list

a trace of inference attempts with a message and optional location for each attempt.

exception TypeError of string * attempt_stack

Raised when the input is ill-typed or could not be inferred.

module Convert (T : Nunchaku_core.TermTyped.S) : sig .. end

module Make (T1 : Nunchaku_core.TermTyped.S)  (T2 : Nunchaku_core.TermInner.S) : sig .. end