inductive Lake.ConfigLang : Type

Lake configuration language identifier.

• lean : ConfigLang
• toml : ConfigLang

@[implicit_reducible]

instance Lake.instReprConfigLang : Repr ConfigLang

Equations

• Lake.instReprConfigLang = { reprPrec := Lake.instReprConfigLang.repr }

def Lake.instReprConfigLang.repr : ConfigLang → Nat → Std.Format

Equations

• Lake.instReprConfigLang.repr Lake.ConfigLang.lean prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.ConfigLang.lean")).group prec✝
• Lake.instReprConfigLang.repr Lake.ConfigLang.toml prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.ConfigLang.toml")).group prec✝

@[implicit_reducible]

instance Lake.instDecidableEqConfigLang : DecidableEq ConfigLang

Equations

• Lake.instDecidableEqConfigLang x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev Lake.ConfigLang.default : ConfigLang

Lake's default configuration language.

Equations

• Lake.ConfigLang.default = Lake.ConfigLang.toml

@[implicit_reducible]

instance Lake.instInhabitedConfigLang : Inhabited ConfigLang

Equations

• Lake.instInhabitedConfigLang = { default := Lake.ConfigLang.default }

def Lake.ConfigLang.ofString? : String → Option ConfigLang

Equations

• Lake.ConfigLang.ofString? "lean" = some Lake.ConfigLang.lean
• Lake.ConfigLang.ofString? "toml" = some Lake.ConfigLang.toml
• Lake.ConfigLang.ofString? x✝ = none

def Lake.ConfigLang.fileExtension : ConfigLang → String

Equations

• Lake.ConfigLang.lean.fileExtension = "lean"
• Lake.ConfigLang.toml.fileExtension = "toml"

@[implicit_reducible]

instance Lake.instToStringConfigLang : ToString ConfigLang

Equations

• Lake.instToStringConfigLang = { toString := Lake.ConfigLang.fileExtension }