package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.kernel/Context/Rel/index.html

Module Context.RelSource

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, 'r) pt = ('constr, 'types, 'r) 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, 'r) pt

empty rel-context

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

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

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

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

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

Check whether given two rel-contexts are equal.

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

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

Sourceval lookup : int -> ('c, 't, 'r) pt -> ('c, 't, 'r) 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, 'r) pt -> ('c, 'c, 'r) pt

Map all terms in a given rel-context.

Sourceval map_with_relevance : ('r -> 'r) -> ('c -> 'c) -> ('c, 'c, 'r) pt -> ('c, 'c, 'r) pt

Map all terms in a given rel-context.

Sourceval map_het : ('r1 -> 'r2) -> ('c -> 'd) -> ('c, 'c, 'r1) pt -> ('d, 'd, 'r2) pt

Map all terms in a given named-context.

Sourceval map_with_binders : (int -> 'c -> 'c) -> ('c, 'c, 'r) pt -> ('c, 'c, 'r) pt

Map all terms in a given rel-context taking into account the position of the binder in the context starting at 1.

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

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

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

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

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

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

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

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

Sourceval to_tags : ('c, 't, 'r) 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. The resulting list is in reverse order compared to the order of declarations in the context.

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

Turn all LocalDef into LocalAssum, leave LocalAssum unchanged.

Sourceval chop_nhyps : int -> ('c, 't, 'r) pt -> ('c, 't, 'r) pt * ('c, 't, 'r) pt

chop_nhyps n Γ returns Γ'',Γ' such that Γ=Γ'Γ'', Γ'' has n hypotheses (i.e. LocalAssum), excluding local definitions (i.e. LocalDef), and Γ'', if n non zero, starts with an hypothesis (i.e., Γ'' has the form x:A;Γ''', i.e., local definitions at the junction of the n hypotheses are put in Γ' rather than in Γ''

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

instance 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 instance_list : (int -> 'v) -> int -> ('c, 't, 'r) pt -> 'v list

instance_list is like instance but returning a list.

Sourceval to_extended_vect : (int -> 'r) -> int -> ('c, 't, 'r) pt -> 'r array
  • deprecated (8.15) Use synonymous [Context.Rel.instance]
Sourceval to_extended_list : (int -> 'r) -> int -> ('c, 't, 'r) pt -> 'r list
  • deprecated (8.15) Use synonymous [Context.Rel.instance_list]