package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type scope_name = string
type tmp_scope_name = scope_name
type subscopes = tmp_scope_name option * scope_name list
type extended_subscopes = Constrexpr.notation_entry_level * subscopes
type constr_as_binder_kind =
  1. | AsIdent
  2. | AsName
  3. | AsNameOrPattern
  4. | AsStrictPattern
type notation_binder_source =
  1. | NtnParsedAsPattern of bool
  2. | NtnParsedAsIdent
  3. | NtnParsedAsName
  4. | NtnBinderParsedAsConstr of constr_as_binder_kind
  5. | NtnParsedAsBinder
type notation_var_instance_type =
  1. | NtnTypeConstr
  2. | NtnTypeBinder of notation_binder_source
  3. | NtnTypeConstrList
  4. | NtnTypeBinderList
type notation_var_internalization_type =
  1. | NtnInternTypeAny
  2. | NtnInternTypeOnlyBinder
type reversibility_status =
  1. | APrioriReversible
  2. | HasLtac
  3. | NonInjective of Names.Id.t list
type notation_interp_env = {
  1. ninterp_var_type : notation_var_internalization_type Names.Id.Map.t;
  2. ninterp_rec_vars : Names.Id.t Names.Id.Map.t;
}
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