def Lake.DSL.packageDeclName : Lean.Name

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

@[reducible, inline]

abbrev Lake.DSL.DocComment : Type

@[reducible, inline]

abbrev Lake.DSL.Attributes : Type

@[reducible, inline]

abbrev Lake.DSL.AttrInstance : Type

@[reducible, inline]

abbrev Lake.DSL.WhereDecls : Type

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

def Lake.DSL.identOrStr : Lean.ParserDescr

@[reducible, inline]

abbrev Lake.DSL.IdentOrStr : Type

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

def Lake.DSL.declField : Lean.ParserDescr

A field assignment in a declarative configuration.

@[reducible, inline]

abbrev Lake.DSL.DeclField : Type

A field assignment in a declarative configuration.

def Lake.DSL.structVal : Lean.ParserDescr

def Lake.DSL.declValDo : Lean.ParserDescr

def Lake.DSL.declValStruct : Lean.ParserDescr

def Lake.DSL.declValWhere : Lean.ParserDescr

def Lake.DSL.simpleDeclSig : Lean.ParserDescr

def Lake.DSL.optConfig : Lean.ParserDescr

@[reducible, inline]

abbrev Lake.DSL.OptConfig : Type

def Lake.DSL.bracketedSimpleBinder : Lean.ParserDescr

def Lake.DSL.simpleBinder : Lean.ParserDescr

@[reducible, inline]

abbrev Lake.DSL.SimpleBinder : Type

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

structure Lake.DSL.Field : Type

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

def Lake.DSL.mkConfigFields (tyName : Lean.Name) (infos : Lean.NameMap ConfigFieldInfo) (fs : Array DeclField) : Lean.Elab.Command.CommandElabM (Lean.TSyntax `Lean.Parser.Term.structInstFields)

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

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