package coq-core

  1. Overview
  2. No Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (11)

Authors

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

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b

doc/coq-core.interp/Notationextern/index.html

Module NotationexternSource

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

Equality on interpretation.

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

Equality on notation_entry_level.

Sourcetype 'a interp_rule_gen =
  1. | NotationRule of Constrexpr.specific_notation
  2. | AbbrevRule of 'a

Binds a notation in a given scope to an interpretation

Sourceval remove_uninterpretation : interp_rule -> Notation_term.interpretation -> unit
Sourceval declare_uninterpretation : ?also_in_cases_pattern:bool -> interp_rule -> Notation_term.interpretation -> unit
Sourcetype notation_applicative_status =
  1. | AppBoundedNotation of int
  2. | AppUnboundedNotation
  3. | NotAppNotation
Sourcetype key

Return printing key

Sourceval glob_prim_constr_key : 'a Glob_term.glob_constr_g -> Names.GlobRef.t option
Sourceval glob_constr_keys : Glob_term.glob_constr -> key list
Sourceval cases_pattern_key : Glob_term.cases_pattern -> key
Sourceval uninterp_notations : 'a Glob_term.glob_constr_g -> notation_rule list

Return the possible notations for a given term

Sourceval 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 =
  1. | OnlyPrinting
  2. | OnlyParsing
  3. | ParsingAndPrinting

Miscellaneous