val create :
?def_as_rewrite:bool ->
?default:type_ ->
?on_var:[ `Default | `Infer ] ->
?on_undef:[ `Warn | `Fail | `Guess ] ->
?on_shadow:[ `Warn | `Ignore ] ->
implicit_ty_args:bool ->
unit ->
tNew context with a signature and default types.
which types are inferred by default (if not provided then type_erm will be used)
if true, definitions will be treated like rewrite rules
behavior when an undefined identifier is met
if true, interpret some constants as in TPTP
behavior when a variable without type annotation is met
val exit_scope : t -> unitExit the current scope (formula, clause), meaning that all free variables' types are forgotten. Some free variables are bound to the default type provided at creation of the context. Some ree variables will be generalized, i.e., kept as (free) variables
Declare the type of a symbol, possibly shadowing a previous version
Execute a function f with an additional declared variable
Execute a function f with additional declared variables