def Lake.DSL.packageDeclName : Lean.Name

The name given to the definition created by the package syntax.

Equations

• Lake.DSL.packageDeclName = `_package

@[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 Attributes) : Array 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 : 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.optConfig : Lean.ParserDescr

Equations

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

@[reducible, inline]

abbrev Lake.DSL.OptConfig : Type

Equations

• Lake.DSL.OptConfig = Lean.TSyntax `Lake.DSL.optConfig

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 SimpleBinder) : Lean.MacroM FunBinder

Equations

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

def Lake.DSL.mkConfigDeclIdent (stx? : Option IdentOrStr) : Lean.Elab.Command.CommandElabM Lean.Ident

Equations

• Lake.DSL.mkConfigDeclIdent (some stx) = pure (Lake.DSL.expandIdentOrStrAsIdent stx)
• Lake.DSL.mkConfigDeclIdent none = do let __do_lift ← Lean.getRef Lean.Elab.Term.mkFreshIdent __do_lift

def Lake.DSL.elabConfig (tyName : Lean.Name) [info : ConfigInfo tyName] (id : Lean.Ident) (ty : Lean.Term) (config : OptConfig) : Lean.Elab.Command.CommandElabM PUnit

Equations

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