package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.17.0.tar.gz
sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250
doc/coq-core.interp/Notation_ops/index.html
Module Notation_opsSource
Utilities about notation_constr
Source
val eq_notation_constr :
(Names.Id.t list * Names.Id.t list) ->
Notation_term.notation_constr ->
Notation_term.notation_constr ->
boolSource
val strictly_finer_notation_constr :
(Names.Id.t list * Names.Id.t list) ->
Notation_term.notation_constr ->
Notation_term.notation_constr ->
boolTell if t1 is a strict refinement of t2 (this is a partial order and returning false does not mean that t2 is finer than t1)
Source
val strictly_finer_interpretation_than :
Notation_term.interpretation ->
Notation_term.interpretation ->
boolTell if a notation interpretation is strictly included in another one
Source
val finer_interpretation_than :
Notation_term.interpretation ->
Notation_term.interpretation ->
boolTell if a notation interpretation is included in another one
Substitution of kernel names in interpretation data
Source
val subst_interpretation :
Mod_subst.substitution ->
Notation_term.interpretation ->
Notation_term.interpretationName of the special identifier used to encode recursive notations
Translation back and forth between glob_constr and notation_constr
Translate a glob_constr into a notation given the list of variables bound by the notation; also interpret recursive patterns
Source
val notation_constr_of_glob_constr :
Notation_term.notation_interp_env ->
Glob_term.glob_constr ->
Notation_term.notation_constr * Notation_term.reversibility_statusRe-interpret a notation as a glob_constr, taking care of binders
Source
type 'a binder_status_fun = {no : 'a -> 'a;restart_prod : 'a -> 'a;restart_lambda : 'a -> 'a;switch_prod : 'a -> 'a;switch_lambda : 'a -> 'a;slide : 'a -> 'a;
}Source
val apply_cases_pattern :
?loc:Loc.t ->
((Names.Id.t list * Glob_term.cases_pattern_disjunction) * Names.Id.t) ->
Glob_term.glob_constr ->
Glob_term.glob_constrSource
val glob_constr_of_notation_constr_with_binders :
?loc:Loc.t ->
('a ->
Names.Name.t ->
Glob_term.glob_constr option ->
'a
* ((Names.Id.t list * Glob_term.cases_pattern_disjunction) * Names.Id.t)
option
* Names.Name.t
* Glob_term.binding_kind
* Glob_term.glob_constr option) ->
('a -> Notation_term.notation_constr -> Glob_term.glob_constr) ->
?h:'a binder_status_fun ->
'a ->
Notation_term.notation_constr ->
Glob_term.glob_constrSource
val glob_constr_of_notation_constr :
?loc:Loc.t ->
Notation_term.notation_constr ->
Glob_term.glob_constrMatching a notation pattern against a glob_constr
match_notation_constr matches a glob_constr against a notation interpretation; raise No_match if the matching fails
Source
val match_notation_constr :
print_univ:bool ->
'a Glob_term.glob_constr_g ->
vars:Names.Id.Set.t ->
Notation_term.interpretation ->
((Names.Id.Set.t * 'a Glob_term.glob_constr_g)
* Notation_term.extended_subscopes)
list
* ((Names.Id.Set.t * 'a Glob_term.glob_constr_g list)
* Notation_term.extended_subscopes)
list
* ((Names.Id.Set.t * 'a Glob_term.cases_pattern_disjunction_g)
* Notation_term.extended_subscopes)
list
* ((Names.Id.Set.t * 'a Glob_term.extended_glob_local_binder_g list)
* Notation_term.extended_subscopes)
listSource
val match_notation_constr_cases_pattern :
'a Glob_term.cases_pattern_g ->
Notation_term.interpretation ->
(('a Glob_term.cases_pattern_g * Notation_term.extended_subscopes) list
* ('a Glob_term.cases_pattern_g list * Notation_term.extended_subscopes)
list)
* (bool * int * 'a Glob_term.cases_pattern_g list)Source
val match_notation_constr_ind_pattern :
Names.inductive ->
'a Glob_term.cases_pattern_g list ->
Notation_term.interpretation ->
(('a Glob_term.cases_pattern_g * Notation_term.extended_subscopes) list
* ('a Glob_term.cases_pattern_g list * Notation_term.extended_subscopes)
list)
* (bool * int * 'a Glob_term.cases_pattern_g list)