package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

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

Equality on notation.

Equality on interpretation.

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

Equality on notation_entry_level.

val 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

val level_eq : level -> level -> bool

Equality on level.

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

Equality on entry_relative_level.

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

Binds a notation in a given scope to an interpretation

type interp_rule = Names.KerName.t interp_rule_gen
val remove_uninterpretation : interp_rule -> Notation_term.interpretation -> unit
val declare_uninterpretation : interp_rule -> Notation_term.interpretation -> unit
type notation_applicative_status =
  1. | AppBoundedNotation of int
  2. | AppUnboundedNotation
  3. | NotAppNotation
type key

Return printing key

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

Return the possible notations for a given term

val uninterp_cases_pattern_notations : 'a Glob_term.cases_pattern_g -> notation_rule list
val uninterp_ind_pattern_notations : Names.inductive -> notation_rule list
val with_notation_uninterpretation_protection : ('a -> 'b) -> 'a -> 'b

State protection

type notation_use =
  1. | OnlyPrinting
  2. | OnlyParsing
  3. | ParsingAndPrinting

Miscellaneous

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct