package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

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 `Notationextern`Source

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

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.

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 : 
  ?also_in_cases_pattern:bool ->
  interp_rule ->
  Notation_term.interpretation ->
  unit

Sourcetype notation_applicative_status =

| AppBoundedNotation of int
| AppUnboundedNotation
| NotAppNotation

Source

type notation_rule =
  interp_rule * Notation_term.interpretation * notation_applicative_status

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

Source

val notation_constr_key : 
  Notation_term.notation_constr ->
  key * 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

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module NotationexternSource

Module `Notationextern`Source