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

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