Named (coq-core.Context.Named)

module Declaration : sig ... end

Representation of local declarations.

type ('constr, 'types) pt = ( 'constr, 'types ) Declaration.pt list

Named-context is represented as a list of declarations. Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list.

val empty : ( 'c, 't ) pt

empty named-context

val add : ( 'c, 't ) Declaration.pt -> ( 'c, 't ) pt -> ( 'c, 't ) pt

Return a new named-context enriched by with a given inner-most declaration.

val length : ( 'c, 't ) pt -> int

Return the number of local declarations in a given named-context.

val lookup : Names.Id.t -> ( 'c, 't ) pt -> ( 'c, 't ) Declaration.pt

Return a declaration designated by an identifier of the variable bound in that declaration.

raises Not_found
if the designated identifier is not bound in a given named-context.

val equal : ( 'c -> 'c -> bool ) -> ( 'c, 'c ) pt -> ( 'c, 'c ) pt -> bool

Check whether given two named-contexts are equal.

val map : ( 'c -> 'c ) -> ( 'c, 'c ) pt -> ( 'c, 'c ) pt

Map all terms in a given named-context.

val iter : ( 'c -> unit ) -> ( 'c, 'c ) pt -> unit

Perform a given action on every declaration in a given named-context.

val fold_inside : 
  ( 'a -> ( 'c, 't ) Declaration.pt -> 'a ) ->
  init:'a ->
  ( 'c, 't ) pt ->
  'a

Reduce all terms in a given named-context to a single value. Innermost declarations are processed first.

val fold_outside : 
  ( ( 'c, 't ) Declaration.pt -> 'a -> 'a ) ->
  ( 'c, 't ) pt ->
  init:'a ->
  'a

Reduce all terms in a given named-context to a single value. Outermost declarations are processed first.

val to_vars : ( 'c, 't ) pt -> Names.Id.Set.t

Return the set of all identifiers bound in a given named-context.

val drop_bodies : ( 'c, 't ) pt -> ( 'c, 't ) pt

Turn all LocalDef into LocalAssum, leave LocalAssum unchanged.

val to_instance : ( Names.Id.t -> 'r ) -> ( 'c, 't ) pt -> 'r list

to_instance Ω builds an instance args in reverse order such that Ω ⊢ args:Ω where Ω is a named-context and with the local definitions of Ω skipped. Example: for id1:T,id2:=c,id3:U, it gives Var id1, Var id3. All idj are supposed distinct.

val instance : ( Names.Id.t -> 'r ) -> ( 'c, 't ) pt -> 'r array

instance Ω builds an instance args such that Ω ⊢ args:Ω where Ω is a named-context and with the local definitions of Ω skipped. Example: for the context id1:T,id2:=c,id3:U (which is internally represented by a list with id3 at the head), it gives Var id1, Var id3. All idj are supposed distinct.

val instance_list : ( Names.Id.t -> 'r ) -> ( 'c, 't ) pt -> 'r list

instance_list is like instance but returning a list.