Documentation

Lean.Parser.Attr

@[inline]

def Lean.Parser.priorityParser (rbp : optParam Nat 0) :

Lean.Parser.Parser

Equations

Lean.Parser.priorityParser rbp = Lean.Parser.categoryParser `prio rbp

@[inline]

def Lean.Parser.attrParser (rbp : optParam Nat 0) :

Lean.Parser.Parser

Equations

Lean.Parser.attrParser rbp = Lean.Parser.categoryParser `attr rbp

def Lean.Parser.Priority.numPrio :

Lean.Parser.Parser

Equations

Lean.Parser.Priority.numPrio = HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.maxPrec) fun x => Lean.Parser.numLit

def Lean.Parser.Attr.simple :

Lean.Parser.Parser

Equations

Lean.Parser.Attr.simple = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "simple" (some `Lean.Parser.Attr.simple)) (Lean.Parser.leadingNode `Lean.Parser.Attr.simple 1024 (HAndThen.hAndThen Lean.Parser.ident fun x => Lean.Parser.optional (HOrElse.hOrElse Lean.Parser.priorityParser fun x => Lean.Parser.ident)))

def Lean.Parser.Attr.macro :

Lean.Parser.Parser

Equations

Lean.Parser.Attr.macro = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "macro" (some `Lean.Parser.Attr.macro)) (Lean.Parser.leadingNode `Lean.Parser.Attr.macro 1024 (HAndThen.hAndThen (Lean.Parser.symbol "macro ") fun x => Lean.Parser.ident))

def Lean.Parser.Attr.export :

Lean.Parser.Parser

Equations

Lean.Parser.Attr.export = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "export" (some `Lean.Parser.Attr.export)) (Lean.Parser.leadingNode `Lean.Parser.Attr.export 1024 (HAndThen.hAndThen (Lean.Parser.symbol "export ") fun x => Lean.Parser.ident))

def Lean.Parser.Attr.recursor :

Lean.Parser.Parser

Equations

Lean.Parser.Attr.recursor = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "recursor" (some `Lean.Parser.Attr.recursor)) (Lean.Parser.leadingNode `Lean.Parser.Attr.recursor 1024 (HAndThen.hAndThen (Lean.Parser.nonReservedSymbol "recursor ") fun x => Lean.Parser.numLit))

def Lean.Parser.Attr.class :

Lean.Parser.Parser

Equations

Lean.Parser.Attr.class = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "class" (some `Lean.Parser.Attr.class)) (Lean.Parser.leadingNode `Lean.Parser.Attr.class 1024 (Lean.Parser.symbol "class"))

def Lean.Parser.Attr.instance :

Lean.Parser.Parser

Equations

Lean.Parser.Attr.instance = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "instance" (some `Lean.Parser.Attr.instance)) (Lean.Parser.leadingNode `Lean.Parser.Attr.instance 1024 (HAndThen.hAndThen (Lean.Parser.symbol "instance") fun x => Lean.Parser.optional Lean.Parser.priorityParser))

def Lean.Parser.Attr.defaultInstance :

Lean.Parser.Parser

Equations

Lean.Parser.Attr.defaultInstance = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "defaultInstance" (some `Lean.Parser.Attr.defaultInstance)) (Lean.Parser.leadingNode `Lean.Parser.Attr.defaultInstance 1024 (HAndThen.hAndThen (Lean.Parser.nonReservedSymbol "defaultInstance ") fun x => Lean.Parser.optional Lean.Parser.priorityParser))

def Lean.Parser.Attr.externEntry :

Lean.Parser.Parser

Equations

Lean.Parser.Attr.externEntry = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "externEntry" (some `Lean.Parser.Attr.externEntry)) (Lean.Parser.leadingNode `Lean.Parser.Attr.externEntry 1024 (HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.ident) fun x => HAndThen.hAndThen (Lean.Parser.optional (Lean.Parser.nonReservedSymbol "inline ")) fun x => Lean.Parser.strLit))

def Lean.Parser.Attr.extern :

Lean.Parser.Parser

Equations

Lean.Parser.Attr.extern = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "extern" (some `Lean.Parser.Attr.extern)) (Lean.Parser.leadingNode `Lean.Parser.Attr.extern 1024 (HAndThen.hAndThen (Lean.Parser.nonReservedSymbol "extern ") fun x => HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.numLit) fun x => Lean.Parser.many Lean.Parser.Attr.externEntry))