Module `Syntax_def`

type syndef_interpretation = (Names.Id.t * Notation_term.subscopes) list * Notation_term.notation_constr

val declare_syntactic_definition : local:bool -> Deprecation.t option -> Names.Id.t -> onlyparsing:bool -> syndef_interpretation -> unit
val search_syntactic_definition : ?⁠loc:Loc.t -> Names.KerName.t -> syndef_interpretation
val search_filtered_syntactic_definition : ?⁠loc:Loc.t -> (syndef_interpretation -> 'a option) -> Names.KerName.t -> 'a option