source
def Lean.Elab.Command.addInheritDocDefault (rhs : Term) (attrs? : Option (Syntax.TSepArray `Lean.Parser.Term.attrInstance ",")) :
Option (Syntax.TSepArray `Lean.Parser.Term.attrInstance ",")
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Command.expandNotationItemIntoSyntaxItem :
TSyntax `Lean.Parser.Command.notationItem → MacroM (TSyntax `stx)

Convert `notation` command lhs item into a `syntax` command item

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Command.expandNotationItemIntoPattern (stx : Syntax) :
MacroM Syntax

Convert `notation` command lhs item into a pattern element

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Command.removeParenthesesAux (parens body : Syntax) :
Syntax
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
partial def Lean.Elab.Command.removeParentheses (stx : Syntax) :
MacroM Syntax
source
def Lean.Elab.Command.hasDuplicateAntiquot (stxs : Array Syntax) :
Bool
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Command.mkUnexpander (attrKind : TSyntax `Lean.Parser.Term.attrKind) (pat qrhs : Term) :
OptionT MacroM Syntax

Try to derive an unexpander from a notation. The notation must be of the form `notation ... => c body` where `c` is a declaration in the current scope and `body` any syntax that contains each variable from the LHS at most once.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Command.elabNotation :
CommandElab
Equations

- One or more equations did not get rendered due to their size.

Instances For