val empty_env : envThe empty/initial environment
val type_expr :
env ->
(Symbols.t * Ty.t) list ->
Parsed.lexpr ->
int Typed.attermTypecheck an input expression (i.e. term (or formula ?)), given a local environment and a list of local types used to extend the initial environment.
Typing_error val type_parsed :
env ->
env Stdlib.Stack.t ->
Parsed.decl ->
int Typed.atdecl list * envType a single declaration.
Typing_error val type_file : Parsed.file -> (int Typed.atdecl * env) list * envType an input file. Returns the successive global environments obtained after typing each declaration.
Typing_error val split_goals :
(int Typed.atdecl * 'a) list ->
((int Typed.atdecl * 'a) list * string) listval split_goals_and_cnf :
(int Typed.atdecl * 'a) list ->
(Commands.sat_tdecl list * string) list