@[reducible, inline]
Equations
- Lake.DSL.DocComment = Lean.TSyntax `Lean.Parser.Command.docComment
@[reducible, inline]
Equations
- Lake.DSL.Attributes = Lean.TSyntax `Lean.Parser.Term.attributes
@[reducible, inline]
Equations
- Lake.DSL.AttrInstance = Lean.TSyntax `Lean.Parser.Term.attrInstance
@[reducible, inline]
Equations
- Lake.DSL.WhereDecls = Lean.TSyntax `Lean.Parser.Term.whereDecls
Equations
- One or more equations did not get rendered due to their size.
- Lake.DSL.expandAttrs attrs? = #[]
Equations
- Lake.DSL.identOrStr = Lean.ParserDescr.nodeWithAntiquot "identOrStr" `Lake.DSL.identOrStr (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.const `ident) (Lean.ParserDescr.const `str))
@[reducible, inline]
Equations
- Lake.DSL.IdentOrStr = Lean.TSyntax `Lake.DSL.identOrStr
Equations
- One or more equations did not get rendered due to their size.
A field assignment in a declarative configuration.
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
A field assignment in a declarative configuration.
Equations
- Lake.DSL.DeclField = Lean.TSyntax `Lake.DSL.declField
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lake.DSL.simpleBinder = Lean.ParserDescr.nodeWithAntiquot "simpleBinder" `Lake.DSL.simpleBinder (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.const `ident) Lake.DSL.bracketedSimpleBinder)
@[reducible, inline]
Equations
- Lake.DSL.SimpleBinder = Lean.TSyntax `Lake.DSL.simpleBinder
Equations
- One or more equations did not get rendered due to their size.
def
Lake.DSL.elabConfigDecl
(tyName : Lean.Name)
(sig : Lean.TSyntax `Lake.DSL.structDeclSig)
(doc? : Option Lake.DSL.DocComment)
(attrs : Array Lake.DSL.AttrInstance)
(name? : Option Lean.Name := none)
: