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
• arity : Nat

@[instance_reducible]

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.