- get (cfg : σ) : α
- set (val : α) (cfg : σ) : σ
- modify (f : α → α) (cfg : σ) : σ
- mkDefault : σ → α
Instances For
@[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)
- mkDefault : σ → ρ
Instances
- fields : Array ConfigFieldInfo
- fieldMap : Lean.NameMap ConfigFieldInfo
Instances
instance
Lake.instConfigFieldOfConfigParent
{σ : Type u_1}
{ρ : Type u_2}
{name : Lean.Name}
{α : Type u_3}
[parent : ConfigParent σ ρ]
[field : ConfigField ρ name α]
:
ConfigField σ name α
Equations
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
instance
Lake.instCoeIdentTSyntaxConsSyntaxNodeKindMkStr4Nil_lake :
Coe Lean.Ident (Lean.TSyntax `Lean.Parser.Term.structInstLVal)