package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (5)

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

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

Module NotationexternSource

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

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

Equality on notation_entry.

Sourceval notation_entry_compare : Constrexpr.notation_entry -> Constrexpr.notation_entry -> int
Sourceval notation_eq : Constrexpr.notation -> Constrexpr.notation -> bool

Equality on notation.

Sourceval notation_compare : Constrexpr.notation -> Constrexpr.notation -> int
Sourceval specific_notation_compare : Constrexpr.specific_notation -> Constrexpr.specific_notation -> int

Equality on notation_binder_kind.

Equality on interpretation.

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

Equality on notation_entry_level.

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

Equality on notation_entry_relative_level.

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

Sourceval level_eq : level -> level -> bool

Equality on level.

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

Equality on entry_relative_level.

Sourcetype interp_rule =
  1. | NotationRule of Constrexpr.specific_notation
  2. | AbbrevRule of Globnames.abbreviation

Binds a notation in a given scope to an interpretation

Sourceval remove_uninterpretation : Environ.env -> interp_rule -> Notation_term.interpretation -> unit
Sourceval declare_uninterpretation : Environ.env -> interp_rule -> Notation_term.interpretation -> unit
Sourcetype notation_applicative_status =
  1. | AppBoundedNotation of int
  2. | AppUnboundedNotation
  3. | NotAppNotation
Sourcetype notation_rule = {
  1. not_rule : interp_rule;
  2. not_patt : Notation_term.interpretation;
  3. not_status : notation_applicative_status;
}
Sourceval uninterp_notations : Environ.env -> 'a Glob_term.glob_constr_g -> notation_rule list

Return the possible notations for a given term

Sourceval uninterp_cases_pattern_notations : Environ.env -> 'a Glob_term.cases_pattern_g -> notation_rule list
Sourceval uninterp_ind_pattern_notations : Environ.env -> 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