@[inline, reducible]

abbrev Lake.DSL.DocComment : Type

Equations

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

@[inline, reducible]

abbrev Lake.DSL.Attributes : Type

Equations

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

@[inline, reducible]

abbrev Lake.DSL.AttrInstance : Type

Equations

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

@[inline, reducible]

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.

def Lake.DSL.declField : Lean.ParserDescr

Equations

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

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.declValTyped : Lean.ParserDescr

Equations

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

def Lake.DSL.declValOptTyped : 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

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

@[inline, reducible]

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.

def Lake.DSL.fixName (id : Lean.Ident) : Option Lake.Name → Lean.Ident

Equations

• Lake.DSL.fixName id x = match x with | some n => Lean.mkIdentFrom id.raw n | none => id

def Lake.DSL.expandDeclField : Lean.TSyntax `Lake.DSL.declField → Lean.MacroM (Lean.TSyntax `Lean.Parser.Term.structInstField)

Equations

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

def Lake.DSL.mkConfigDecl (name? : Option Lake.Name) (doc? : Option Lake.DSL.DocComment) (attrs : Array Lake.DSL.AttrInstance) (ty : Lean.Term) (spec : Lean.Syntax) : Lean.MacroM Lean.Command

Equations

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