Documentation

Lake.Config.Meta

source
structure Lake.ConfigProj (σ : Type u) (α : Type v) :
Type (max u v)
  • get (cfg : σ) : α
  • set (val : α) (cfg : σ) : σ
  • modify (f : α → α) (cfg : σ) : σ
  • mkDefault : σ → α
source
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 : σ → α
Instances
source
@[reducible, inline]
abbrev Lake.mkFieldDefault {σ : Type u_1} {α : Type u_2} (name : Lean.Name) [field : ConfigField σ name α] (cfg : σ) :
α
Equations
source
class Lake.ConfigParent (σ : Type u) (ρ : semiOutParam (Type v)) extends Lake.ConfigProj σ ρ :
Type (max u v)
  • get (cfg : σ) : ρ
  • set (val : ρ) (cfg : σ) : σ
  • modify (f : ρ → ρ) (cfg : σ) : σ
  • mkDefault : σ → ρ
Instances
source
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.

source
class Lake.ConfigFields (σ : Type u) :
Type
Instances
source
class Lake.ConfigInfo (name : Lean.Name) :
Type
Instances
source
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.
source
def Lake.configField :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
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.
source
def Lake.expandConfigDecl :
Lean.Macro
Equations
  • One or more equations did not get rendered due to their size.