Functor TypeCheck.Make

module Make (T : TermInner.S) : sig .. end

Parameters:

T : TermInner.S

type t

val empty : ?check_non_empty_tys:bool ->
       ?env:(T.t, T.t) Env.t -> unit -> t

val check_statement : t -> (T.t, T.t) Statement.t -> t

check_statement t st checks that st is well typed and well-formed, and then return a new t that can be used to check subsequent statements

val check_problem : t -> (T.t, T.t) Problem.t -> unit

Check invariants on all the problem's statements