TOML Decoders

This module contains definitions to assist in decoding TOML data values into concrete user types.

structure Lake.Toml.DecodeError : Type

• ref : Lean.Syntax
• msg : String

@[reducible, inline]

abbrev Lake.Toml.DecodeM (α : Type) : Type

@[reducible, inline]

abbrev Lake.Toml.EDecodeM (α : Type) : Type

class Lake.DecodeToml (α : Type) : Type

• decode (v : Toml.Value) : Toml.EDecodeM α

@[reducible, inline]

abbrev Lake.decodeToml {α : Type} [DecodeToml α] (v : Toml.Value) : Toml.EDecodeM α

@[inline]

def Lake.Toml.ensureDecode {α : Type} (x : DecodeM α) : EDecodeM α

Run the decode action. If there were errors, throw. Otherwise, return the result.

@[inline]

def Lake.Toml.tryDecodeD {α : Type} (default : α) (x : EDecodeM α) : DecodeM α

Run the decode action. If it fails, keep the errors but return default.

@[inline]

def Lake.Toml.tryDecode? {α : Type} (x : EDecodeM α) : DecodeM (Option α)

Run the decode action. If it fails, keep the errors but return none.

@[inline]

def Lake.Toml.tryDecode {α : Type} [Inhabited α] (x : EDecodeM α) : DecodeM α

Run the decode action. If it fails, keep the errors but return Inhabited.default.

@[inline]

def Lake.Toml.optDecodeD {β : Type} {α : Type u_1} (default : β) (a? : Option α) (f : α → EDecodeM β) : DecodeM β

If the value is not none, run the decode action. If it fails, add the errors to the state and return default.

@[inline]

def Lake.Toml.optDecode {β : Type} {α : Type u_1} [Inhabited β] (a? : Option α) (f : α → EDecodeM β) : DecodeM β

If the value is not none, run the decode action. If it fails, add the errors to the state and return Inhabited.default.

@[inline]

def Lake.Toml.optDecode? {α : Type u_1} {β : Type} (a? : Option α) (f : α → EDecodeM β) : DecodeM (Option β)

If the value is not none, run the decode action. If it fails, add the errors to the state and return none. Otherwise, return the result in some.

def Lake.Toml.mergeErrors {α β γ : Type} (x₁ : EDecodeM α) (x₂ : EDecodeM β) (f : α → β → γ) : EDecodeM γ

If either action errors, throw the concatenated errors. Otherwise, if no errors, combine the results with f.

@[inline]

def Lake.Toml.throwDecodeErrorAt {α : Type} (ref : Lean.Syntax) (msg : String) : EDecodeM α

def Lake.Toml.decodeArray {α : Type} [dec : DecodeToml α] (vs : Array Value) : EDecodeM (Array α)

Decode an array of TOML values, merging any errors from the elements into a single array.

def Lake.Toml.Value.decodeString (v : Value) : EDecodeM String

instance Lake.Toml.Value.instDecodeTomlString : DecodeToml String

instance Lake.Toml.Value.instDecodeTomlFilePath : DecodeToml System.FilePath

def Lake.Toml.Value.decodeName (v : Value) : EDecodeM Lean.Name

instance Lake.Toml.Value.instDecodeTomlName : DecodeToml Lean.Name

def Lake.Toml.Value.decodeInt (v : Value) : EDecodeM Int

instance Lake.Toml.Value.instDecodeTomlInt : DecodeToml Int

def Lake.Toml.Value.decodeNat : Value → EDecodeM Nat

instance Lake.Toml.Value.instDecodeTomlNat : DecodeToml Nat

def Lake.Toml.Value.decodeFloat (v : Value) : EDecodeM Float

instance Lake.Toml.Value.instDecodeTomlFloat : DecodeToml Float

def Lake.Toml.Value.decodeBool (v : Value) : EDecodeM Bool

instance Lake.Toml.Value.instDecodeTomlBool : DecodeToml Bool

def Lake.Toml.Value.decodeDateTime (v : Value) : EDecodeM DateTime

instance Lake.Toml.Value.instDecodeTomlDateTime : DecodeToml DateTime

def Lake.Toml.Value.decodeValueArray (v : Value) : EDecodeM (Array Value)

@[inline]

def Lake.Toml.Value.decodeArray {α : Type} [dec : DecodeToml α] (v : Value) : EDecodeM (Array α)

instance Lake.Toml.Value.instDecodeTomlArray {α : Type} [DecodeToml α] : DecodeToml (Array α)

@[inline]

def Lake.Toml.Value.decodeArrayOrSingleton {α : Type} [dec : DecodeToml α] (v : Value) : EDecodeM (Array α)

def Lake.Toml.Value.decodeTable (v : Value) : EDecodeM Table

def Lake.Toml.decodeKeyval {α : Type} [dec : DecodeToml α] (k : Lean.Name) (v : Value) : EDecodeM α

def Lake.Toml.Table.decodeValue (t : Table) (k : Lean.Name) (ref : Lean.Syntax := Lean.Syntax.missing) : EDecodeM Value

@[inline]

def Lake.Toml.Table.decode {α : Type} [dec : DecodeToml α] (t : Table) (k : Lean.Name) (ref : Lean.Syntax := Lean.Syntax.missing) : EDecodeM α

@[inline]

def Lake.Toml.Table.decode? {α : Type} [dec : DecodeToml α] (t : Table) (k : Lean.Name) : EDecodeM (Option α)

def Lake.Toml.Table.decodeNameMap {α : Type} [dec : DecodeToml α] (t : Table) : EDecodeM (Lean.NameMap α)

instance Lake.Toml.Table.instDecodeTomlNameMap {α : Type} [DecodeToml α] : DecodeToml (Lean.NameMap α)

@[inline]

def Lake.Toml.Table.tryDecode {α : Type} [Inhabited α] [dec : DecodeToml α] (t : Table) (k : Lean.Name) (ref : Lean.Syntax := Lean.Syntax.missing) : DecodeM α

@[inline]

def Lake.Toml.Table.tryDecode? {α : Type} [dec : DecodeToml α] (t : Table) (k : Lean.Name) : DecodeM (Option α)

@[inline]

def Lake.Toml.Table.tryDecodeD {α : Type} [dec : DecodeToml α] (k : Lean.Name) (default : α) (t : Table) : DecodeM α