Module LibBinding.State

type state
type 'a t = state -> 'a
val return : 'a -> 'a t
val get_env : Environ.env t
val get_sigma : Evd.evar_map t
val get_names : Nameops.Fresh.t t
val get_state : state t
val make : Environ.env -> Evd.evar_map -> state

Create a new state out of an environment env and evar_map sigma with:

  • The set of names is computed out of env
  • The substitution is empty
Weaken Functions From the Former Context to the New Context

Weaken a term defined in the former context by applying state.subst.

Weaken a declaration defined in the former context by applying state.subst.

val weaken_context : EConstr.rel_context -> EConstr.rel_context t

Weaken a context defined in the former context by applying state.subst.

Push Functions
val push_old_rel : EConstr.rel_declaration -> (state * access_key) t

Add a former definition decl to a state s. It returns the new state, and an access key to acces the declaration. It supposes decl is well-typed in the current context.

val push_fresh_rel : EConstr.rel_declaration -> (state * access_key) t

Add a new definition decl to a state s. It returns the new state, and an access key to acces the declaration. It supposes decl is well-typed in the current context.

Access Functions
Access Terms
val get_term : access_key -> EConstr.constr t

Compute the debruijn variable associated to an access_key in the context s : state.

val geti_term : access_key list -> int -> EConstr.constr t

Compute the debruijn variable associated to the i-th access_key in the context s : state.

val getij_term : access_key list list -> int -> int -> EConstr.constr t

Compute the debruijn variable associated to the i-th, j-th access_key in the context s : state.

val get_terms : access_key list -> EConstr.constr list t

Compute the debruijn variables associated to a list of access_key in the context s : state.

Access Types
val get_type : access_key -> EConstr.types t

Compute the type of the variable associated to an access_key in the context s : state.

val geti_type : access_key list -> int -> EConstr.types t

Compute the type of the variable associated to the i-th access_key in the context s : state.

val getij_type : access_key list list -> int -> int -> EConstr.types t

Compute the type of the variable associated to the i-th, j-th access_key in the context s : state.

val get_types : access_key list -> EConstr.types list t

Compute the type of the variable associated to a list of access_key in the context s : state.

Access Binder Annotations

Compute the binder_annot of the variable associated to an access_key in the context s : state.

val geti_aname : access_key list -> int -> Names.Name.t EConstr.binder_annot t

Compute the binder_annot of the variable associated to the i-th access_key in the context s : state.

val getij_aname : access_key list list -> int -> int -> Names.Name.t EConstr.binder_annot t

Compute the binder_annot of the variable associated to the i-th, j-th access_key in the context s : state.

val get_anames : access_key list -> Names.Name.t EConstr.binder_annot list t

Compute the binder_annot of the variable associated to a list of access_key in the context s : state.

Debug Functions
val print_state : (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> Pp.t t

Print function for debugging.