Module LibBinding.State

type state
type 'a t
val return : 'a -> 'a t
val bind : 'a t -> ('a -> 'b t) -> 'b t
val map : ('a -> 'b) -> 'a t -> 'b t
val run_state : state -> Evd.evar_map -> 'a t -> Evd.evar_map * 'a
val run : Environ.env -> Evd.evar_map -> 'a t -> Evd.evar_map * 'a
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 get_context : EConstr.rel_context t
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.

Access Key
type access_key

Type of access keys for the State API

val make_key : int -> access_key t
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 array 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 array 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 array t

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

Check Keys
val check_key_in : int -> access_key list -> int option t
val list_mapi : (int -> 'a -> 'b t) -> 'a list -> 'b list t

Debug Functions

val list_map2i : (int -> 'a -> 'b -> 'c t) -> 'a list -> 'b list -> 'c list t
val array_mapi : (int -> 'a -> 'b t) -> 'a array -> 'b array t
val array_map2i : (int -> 'a -> 'b -> 'c t) -> 'a array -> 'b array -> 'c array t