Documentation

Lake.Config.Meta

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

            Instances For
              class Lake.ConfigFields (σ : Type u) :
              Instances
                instance Lake.instConfigFieldOfConfigParent {σ : Type u_1} {ρ : Type u_2} {name : Lean.Name} {α : Type u_3} [parent : ConfigParent σ ρ] [field : ConfigField ρ name α] :
                ConfigField σ name α
                Equations
                  Equations
                    Instances For

                      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
                        Instances For
                          Equations
                            Instances For