Module `Context.Rel`Source

Representation of contexts that can capture anonymous as well as non-anonymous variables. Individual declarations are then designated by de Bruijn indexes.

Sourcemodule Declaration : sig ... end

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

Rel-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 rel-context

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

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

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

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

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

Check whether given two rel-contexts are equal.

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

Return the number of local assumptions in a given rel-context.

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

Return a declaration designated by a given de Bruijn index.

raises Not_found
if the designated de Bruijn index outside the range.

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

Map all terms in a given rel-context.

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

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

Source

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

Reduce all terms in a given rel-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 rel-context to a single value. Outermost declarations are processed first.

Sourceval to_tags : ('c, 't) pt -> bool list

Map a given rel-context to a list where each local assumption is mapped to true and each local definition is mapped to false.

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

Turn all LocalDef into LocalAssum, leave LocalAssum unchanged.

Sourceval to_extended_list : (int -> 'r) -> int -> ('c, 't) pt -> 'r list

extended_list mk n Γ builds an instance args such that Γ,Δ ⊢ args:Γ with n = |Δ| and with the local definitions of Γ skipped in args where mk is used to build the corresponding variables. Example: for x:T, y:=c, z:U and n=2, it gives mk 5, mk 3.

Sourceval to_extended_vect : (int -> 'r) -> int -> ('c, 't) pt -> 'r array

extended_vect n Γ does the same, returning instead an array.

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Context.Rel`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Context.RelSource

Module `Context.Rel`Source