package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module LibBinding.StateSource

Sourcetype state
Sourcetype 'a t
Sourceval return : 'a -> 'a t
Sourceval bind : 'a t -> ('a -> 'b t) -> 'b t
Sourceval map : ('a -> 'b) -> 'a t -> 'b t
Sourceval run_state : state -> Evd.evar_map -> 'a t -> Evd.evar_map * 'a
Sourceval run : Environ.env -> Evd.evar_map -> 'a t -> Evd.evar_map * 'a
Sourceval get_env : Environ.env t
Sourceval get_sigma : Evd.evar_map t
Sourceval get_names : Nameops.Fresh.t t
Sourceval get_state : state t
Sourceval 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.

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

Access Key
Sourcetype access_key

Type of access keys for the State API

Sourceval make_key : int -> access_key t
Push Functions

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.

Sourceval 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

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

Sourceval 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.

Sourceval 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.

Sourceval 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
Sourceval get_type : access_key -> EConstr.types t

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

Sourceval 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.

Sourceval 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.

Sourceval 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.

Sourceval 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.

Sourceval 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.

Sourceval 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
Sourceval check_key_in : int -> access_key list -> int option t
Sourceval list_mapi : (int -> 'a -> 'b t) -> 'a list -> 'b list t

Debug Functions

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