@[reducible, inline]

abbrev Lake.DSL.DocComment : Type

Equations

• Lake.DSL.DocComment = Lean.TSyntax `Lean.Parser.Command.docComment

@[reducible, inline]

abbrev Lake.DSL.Attributes : Type

Equations

• Lake.DSL.Attributes = Lean.TSyntax `Lean.Parser.Term.attributes

@[reducible, inline]

abbrev Lake.DSL.AttrInstance : Type

Equations

• Lake.DSL.AttrInstance = Lean.TSyntax `Lean.Parser.Term.attrInstance

@[reducible, inline]

abbrev Lake.DSL.WhereDecls : Type

Equations

• Lake.DSL.WhereDecls = Lean.TSyntax `Lean.Parser.Term.whereDecls

def Lake.DSL.expandAttrs (attrs? : Option Lake.DSL.Attributes) : Array Lake.DSL.AttrInstance

Equations

• One or more equations did not get rendered due to their size.
• Lake.DSL.expandAttrs attrs? = #[]

def Lake.DSL.identOrStr : Lean.ParserDescr

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]

abbrev Lake.DSL.IdentOrStr : Type

Equations

• Lake.DSL.IdentOrStr = Lean.TSyntax `Lake.DSL.identOrStr

def Lake.DSL.expandIdentOrStrAsIdent (stx : Lake.DSL.IdentOrStr) : Lean.Ident

Equations

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

def Lake.DSL.declField : Lean.ParserDescr

A field assignment in a declarative configuration.

Equations

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

@[reducible, inline]

abbrev Lake.DSL.DeclField : Type

A field assignment in a declarative configuration.

Equations

• Lake.DSL.DeclField = Lean.TSyntax `Lake.DSL.declField

def Lake.DSL.structVal : Lean.ParserDescr

Equations

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

def Lake.DSL.declValDo : Lean.ParserDescr

Equations

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

def Lake.DSL.declValStruct : Lean.ParserDescr

Equations

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

def Lake.DSL.declValWhere : Lean.ParserDescr

Equations

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

def Lake.DSL.simpleDeclSig : Lean.ParserDescr

Equations

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

def Lake.DSL.structDeclSig : Lean.ParserDescr

Equations

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

def Lake.DSL.bracketedSimpleBinder : Lean.ParserDescr

Equations

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

def Lake.DSL.simpleBinder : Lean.ParserDescr

Equations

• Lake.DSL.simpleBinder = Lean.ParserDescr.nodeWithAntiquot "simpleBinder" `Lake.DSL.simpleBinder (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.const `ident) Lake.DSL.bracketedSimpleBinder)

@[reducible, inline]

abbrev Lake.DSL.SimpleBinder : Type

Equations

• Lake.DSL.SimpleBinder = Lean.TSyntax `Lake.DSL.simpleBinder

def Lake.DSL.expandOptSimpleBinder (stx? : Option Lake.DSL.SimpleBinder) : Lean.MacroM Lake.FunBinder

Equations

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

structure Lake.DSL.Field : Type

• ref : Lean.Syntax
• val : Lean.Term

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) : Lean.Elab.Command.CommandElabM PUnit