@[reducible, inline]

## Equations

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

## Instances For

@[reducible, inline]

## Equations

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

## Instances For

@[reducible, inline]

## Equations

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

## Instances For

@[reducible, inline]

## Equations

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

## Instances For

## Equations

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

## Instances For

A single field assignment in a declarative configuration.

## Equations

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

## Instances For

@[reducible, inline]

A single field assignment in a declarative configuration.

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

@[reducible, inline]

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

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.

## Instances For

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

## Equations

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