package coq

  1. Overview
  2. Docs
Formal proof management system

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.14.0.tar.gz
sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c

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

Module Syntax_defSource

Syntactic definitions.

Sourceval declare_syntactic_definition : local:bool -> ?also_in_cases_pattern:bool -> Deprecation.t option -> Names.Id.t -> onlyparsing:bool -> Notation_term.interpretation -> unit
Sourceval search_syntactic_definition : ?loc:Loc.t -> Names.KerName.t -> Notation_term.interpretation
Sourceval search_filtered_syntactic_definition : ?loc:Loc.t -> (Notation_term.interpretation -> 'a option) -> Names.KerName.t -> 'a option
OCaml

Innovation. Community. Security.