module type S =`sig`

..`end`

`type `

untyped

untyped term

`type `

typed

typed term

`val infer_exn : ``LogtkTypeInference.Ctx.t ->`

untyped ->

LogtkType.t * typed LogtkTypeInference.Closure.t

Infer the type of this term under the given signature. This updates
the context's typing environment!

**Raises**

**Returns** 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`val infer : ``LogtkTypeInference.Ctx.t ->`

untyped ->

(LogtkType.t * typed LogtkTypeInference.Closure.t)

LogtkTypeInference.or_error

Safe version of

`LogtkTypeInference.S.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.

`val constrain_term_term_exn : ``LogtkTypeInference.Ctx.t ->`

untyped -> untyped -> unit

Force the two terms to have the same type in this context

**Raises**

`LogtkType.Error`

if an inconsistency is detected`val constrain_term_type_exn : ``LogtkTypeInference.Ctx.t ->`

untyped -> LogtkType.t -> unit

Force the term's type and the given type to be the same.

**Raises**

`LogtkType.Error`

if an inconsistency is detected`val constrain_term_term : ``LogtkTypeInference.Ctx.t ->`

untyped ->

untyped -> unit LogtkTypeInference.or_error

Safe version of

`LogtkTypeInference.S.constrain_term_term_exn`

`val constrain_term_type : ``LogtkTypeInference.Ctx.t ->`

untyped ->

LogtkType.t -> unit LogtkTypeInference.or_error

Safe version of

`LogtkTypeInference.S.constrain_term_type_exn`