Module LogtkTypeInference.HO

module HO: sig .. end

include LogtkTypeInference.S
val constrain : ctx:LogtkTypeInference.Ctx.t -> untyped -> unit LogtkTypeInference.or_error
Constrain the term to be well-typed and of boolean type
val convert : ?generalize:bool ->
?ret:LogtkType.t ->
ctx:LogtkTypeInference.Ctx.t -> untyped -> typed LogtkTypeInference.or_error
Convert a single untyped term to a typed term. Binds free constructor variables to default.
generalize : if true, constructor types are generalized (see LogtkTypeInference.FO.convert more more details). Default is false
ret : is the type we expect for this term (default: LogtkType.o)
ctx : context used for type inference
val convert_seq : ?generalize:bool ->
ctx:LogtkTypeInference.Ctx.t ->
untyped Sequence.t -> typed list LogtkTypeInference.or_error
Infer the types of those terms and annotate each term and subterm with its type. Also updates the context's signature. All terms are assumed to be boolean.

Unsafe API

Functions that can raise LogtkType.Error
val constrain_exn : ctx:LogtkTypeInference.Ctx.t -> untyped -> unit
val convert_exn : ?generalize:bool ->
?ret:LogtkType.t -> ctx:LogtkTypeInference.Ctx.t -> untyped -> typed
val convert_seq_exn : ?generalize:bool ->
ctx:LogtkTypeInference.Ctx.t -> untyped Sequence.t -> typed list