structure Lake.ConfigProj (σ : Type u) (α : Type v) : Type (max u v)

• get (cfg : σ) : α
• set (val : α) (cfg : σ) : σ
• modify (f : α → α) (cfg : σ) : σ
• mkDefault : σ → α

class Lake.ConfigField (σ : Type u) (name : Lean.Name) (α : outParam (Type v)) extends Lake.ConfigProj σ α : Type (max u v)

• get (cfg : σ) : α
• set (val : α) (cfg : σ) : σ
• modify (f : α → α) (cfg : σ) : σ
• mkDefault : σ → α

@[reducible, inline]

abbrev Lake.mkFieldDefault {σ : Type u_1} {α : Type u_2} (name : Lean.Name) [field : ConfigField σ name α] (cfg : σ) : α

Equations

• Lake.mkFieldDefault name cfg = (field.toConfigProj name).mkDefault cfg

class Lake.ConfigParent (σ : Type u) (ρ : semiOutParam (Type v)) extends Lake.ConfigProj σ ρ : Type (max u v)

• get (cfg : σ) : ρ
• set (val : ρ) (cfg : σ) : σ
• modify (f : ρ → ρ) (cfg : σ) : σ
• mkDefault : σ → ρ

structure Lake.ConfigFieldInfo : Type

• name : Lean.Name

  The name of the field (possibly an alias).

• realName : Lean.Name

  The real name of the field in the configuration structure.

• canonical : Bool

  Whether name == realName and the field is not a parent projection.

• parent : Bool

  Whether the field is a parent projection.

class Lake.ConfigFields (σ : Type u) : Type

• fields : Array ConfigFieldInfo

class Lake.ConfigInfo (name : Lean.Name) : Type

• fields : Array ConfigFieldInfo
• fieldMap : Lean.NameMap ConfigFieldInfo

instance Lake.instConfigFieldOfConfigParent {σ : Type u_1} {ρ : Type u_2} {name : Lean.Name} {α : Type u_3} [parent : ConfigParent σ ρ] [field : ConfigField ρ name α] : ConfigField σ name α

Equations

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

def Lake.configField : Lean.ParserDescr

Equations

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

def Lake.configDecl : Lean.ParserDescr

An tailored structure command for producing Lake configuration data types. It supports additional field annotations and generates additional metadata used during serialization to/from Lean and TOML.

It is not a perfect superset of structure, but instead just the parts that are / could be reasonably needed by Lake.

Equations

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

instance Lake.instCoeIdentTSyntaxConsSyntaxNodeKindMkStr4Nil_lake : Coe Lean.Ident (Lean.TSyntax `Lean.Parser.Term.structInstLVal)

Equations

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

def Lake.expandConfigDecl : Lean.Macro

Equations

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