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

Equations

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

def Lean.Elab.Command.expandNotationItemIntoSyntaxItem : Lean.TSyntax `Lean.Parser.Command.notationItem → Lean.MacroM (Lean.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.

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

Convert notation command lhs item into a pattern element

Equations

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

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

Equations

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

partial def Lean.Elab.Command.removeParentheses (stx : Lean.Syntax) : Lean.MacroM Lean.Syntax

def Lean.Elab.Command.hasDuplicateAntiquot (stxs : Array Lean.Syntax) : Bool

Equations

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

def Lean.Elab.Command.mkUnexpander (attrKind : Lean.TSyntax `Lean.Parser.Term.attrKind) (pat qrhs : Lean.Term) : OptionT Lean.MacroM Lean.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.

def Lean.Elab.Command.expandNotation : Lean.Macro

Equations

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