package rocq-runtime
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
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.
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.
Return a new rel-context enriched by with a given inner-most declaration.
Return the number of local declarations in a given rel-context.
val equal :
('r -> 'r -> bool) ->
('c -> 'c -> bool) ->
('c, 'c, 'r) pt ->
('c, 'c, 'r) pt ->
boolCheck whether given two rel-contexts are equal.
Return the number of local assumptions in a given rel-context.
Return a declaration designated by a given de Bruijn index.
Map all terms in a given rel-context.
Map all terms in a given rel-context.
Map all terms in a given named-context.
Map all terms in a given rel-context taking into account the position of the binder in the context starting at 1.
Perform a given action on every declaration in a given rel-context.
val fold_inside :
('a -> ('c, 't, 'r) Declaration.pt -> 'a) ->
init:'a ->
('c, 't, 'r) pt ->
'aReduce all terms in a given rel-context to a single value. Innermost declarations are processed first.
val fold_outside :
(('c, 't, 'r) Declaration.pt -> 'a -> 'a) ->
('c, 't, 'r) pt ->
init:'a ->
'aReduce all terms in a given rel-context to a single value. Outermost declarations are processed first.
Return the set of all named variables bound in a given rel-context.
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.
Turn all LocalDef into LocalAssum, leave LocalAssum unchanged.
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 Γ''
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.
instance_list is like instance but returning a list.