package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.16.0.tar.gz
sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587
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)
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)