package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Notation_opsSource

Utilities about notation_constr
Sourceval eq_notation_constr : (Names.Id.t list * Names.Id.t list) -> Notation_term.notation_constr -> Notation_term.notation_constr -> bool
Sourceval strictly_finer_notation_constr : (Names.Id.t list * Names.Id.t list) -> Notation_term.notation_constr -> Notation_term.notation_constr -> bool

Tell if t1 is a strict refinement of t2 (this is a partial order and returning false does not mean that t2 is finer than t1)

Substitution of kernel names in interpretation data

Name of the special identifier used to encode recursive notations

Sourceval ldots_var : Names.Id.t
Translation back and forth between glob_constr and notation_constr

Translate a glob_constr into a notation given the list of variables bound by the notation; also interpret recursive patterns

Re-interpret a notation as a glob_constr, taking care of binders

Sourcetype 'a binder_status_fun = {
  1. no : 'a -> 'a;
  2. restart_prod : 'a -> 'a;
  3. restart_lambda : 'a -> 'a;
  4. switch_prod : 'a -> 'a;
  5. switch_lambda : 'a -> 'a;
  6. slide : 'a -> 'a;
}
Sourceval glob_constr_of_notation_constr : ?loc:Loc.t -> Notation_term.notation_constr -> Glob_term.glob_constr
Matching a notation pattern against a glob_constr

match_notation_constr matches a glob_constr against a notation interpretation; raise No_match if the matching fails

Sourceexception No_match
Sourceval print_parentheses : bool ref
Matching a notation pattern against a glob_constr
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet 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