Module `Context.Named`Source

This module represents contexts that can capture non-anonymous variables. Individual declarations are then designated by the identifiers they bind.

Sourcemodule Declaration : sig ... end

Representation of local declarations.

Sourcetype ('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.

Sourceval empty : ('c, 't) pt

empty named-context

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

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

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

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

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

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

Check whether given two named-contexts are equal.

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

Map all terms in a given named-context.

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

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

Source

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.

Source

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.

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

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

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

Turn all LocalDef into LocalAssum, leave LocalAssum unchanged.

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

deprecated [to_instance] was missing a [List.rev] to comply to its specification; rely on [instance] for the correct specification or use [List.rev (instance ...)] for strict compatibility

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

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

instance_list is like instance but returning a list.

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/Context/Named/index.html

Module `Context.Named`Source

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/Context/Named/index.html

Module Context.NamedSource

Module `Context.Named`Source