Module `Notationextern`Source

Declaration of uninterpretation functions (i.e. printing rules) for notations

val notation_entry_eq : 
  Constrexpr.notation_entry ->
  Constrexpr.notation_entry ->
  bool

Equality on notation_entry.

Source

val notation_with_optional_scope_eq : 
  Constrexpr.notation_with_optional_scope ->
  Constrexpr.notation_with_optional_scope ->
  bool

Sourceval notation_eq : Constrexpr.notation -> Constrexpr.notation -> bool

Equality on notation.

Source

val notation_binder_kind_eq : 
  Notation_term.notation_binder_kind ->
  Notation_term.notation_binder_kind ->
  bool

Equality on notation_binder_kind.

Source

val interpretation_eq : 
  Notation_term.interpretation ->
  Notation_term.interpretation ->
  bool

Equality on interpretation.

Source

val notation_entry_level_eq : 
  Constrexpr.notation_entry_level ->
  Constrexpr.notation_entry_level ->
  bool

Equality on notation_entry_level.

Source

val notation_entry_relative_level_eq : 
  Constrexpr.notation_entry_relative_level ->
  Constrexpr.notation_entry_relative_level ->
  bool

Equality on notation_entry_relative_level.

Source

type level =
  Constrexpr.notation_entry_level * Constrexpr.entry_relative_level list

The "signature" of a rule: its level together with the levels of its subentries

Sourceval level_eq : level -> level -> bool

Equality on level.

Source

val entry_relative_level_eq : 
  Constrexpr.entry_relative_level ->
  Constrexpr.entry_relative_level ->
  bool

Equality on entry_relative_level.

Sourcetype 'a interp_rule_gen =

| NotationRule of Constrexpr.specific_notation
| AbbrevRule of 'a

Binds a notation in a given scope to an interpretation

Sourcetype interp_rule = Names.KerName.t interp_rule_gen

Source

val remove_uninterpretation : 
  interp_rule ->
  Notation_term.interpretation ->
  unit

Source

val declare_uninterpretation : 
  interp_rule ->
  Notation_term.interpretation ->
  unit

Sourcetype notation_applicative_status =

| AppBoundedNotation of int
| AppUnboundedNotation
| NotAppNotation

Sourcetype notation_rule = {

not_rule : interp_rule;
not_patt : Notation_term.interpretation;
not_status : notation_applicative_status;

}

Sourceval uninterp_notations : 'a Glob_term.glob_constr_g -> notation_rule list

Return the possible notations for a given term

Source

val uninterp_cases_pattern_notations : 
  'a Glob_term.cases_pattern_g ->
  notation_rule list

Sourceval uninterp_ind_pattern_notations : Names.inductive -> notation_rule list

Sourceval with_notation_uninterpretation_protection : ('a -> 'b) -> 'a -> 'b

State protection

Sourcetype notation_use =

| OnlyPrinting
| OnlyParsing
| ParsingAndPrinting

Miscellaneous

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.interp/Notationextern/index.html

Module `Notationextern`Source

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.interp/Notationextern/index.html

Module NotationexternSource

Module `Notationextern`Source