TOML Encoders #

This module contains definitions to assist in encoding Lean types into TOML data values.

source

class Lake.ToToml (α : Type u) :

Type u

toToml : α → Toml.Value

Instances

source

instance Lake.instToTomlValue :

ToToml Toml.Value

Equations

source

instance Lake.instToTomlString :

ToToml String

Equations

source

instance Lake.instToTomlFilePath :

ToToml System.FilePath

Equations

source

instance Lake.instToTomlName :

ToToml Lean.Name

Equations

source

instance Lake.instToTomlInt :

ToToml Int

Equations

source

instance Lake.instToTomlNat :

ToToml Nat

Equations

source

instance Lake.instToTomlFloat :

ToToml Float

Equations

source

instance Lake.instToTomlBool :

ToToml Bool

Equations

source

instance Lake.instToTomlArray {α : Type u_1} [ToToml α] :

ToToml (Array α)

Equations

source

instance Lake.instToTomlArrayValue :

ToToml (Array Toml.Value)

Equations

source

instance Lake.instToTomlTable :

ToToml Toml.Table

Equations

source

class Lake.ToToml? (α : Type u) :

Type u

toToml? : α → Option Toml.Value

Instances

source

@[instance 10000]

instance Lake.instToToml?OfToToml {α : Type u_1} [ToToml α] :

ToToml? α

Equations

source

def Lake.Toml.encodeArray? {α : Type u_1} [ToToml? α] (as : Array α) :

Option (Array Value)

Equations

Instances For

source

instance Lake.instToToml?Array {α : Type u_1} [ToToml? α] :

ToToml? (Array α)

Equations

source

instance Lake.instToToml?Option {α : Type u_1} [ToToml? α] :

ToToml? (Option α)

Equations

source

instance Lake.instToToml?OptionOfToToml {α : Type u_1} [ToToml α] :

ToToml? (Option α)

Equations

source

class Lake.Toml.SmartInsert (α : Type u) :

Type u

smartInsert (k : Lean.Name) : α → Table → Table
Insert a value into a table unless it represents a nullish value.

Instances

source

@[instance 100]

instance Lake.Toml.instSmartInsertOfToToml? {α : Type u_1} [ToToml? α] :

SmartInsert α

Equations

source

instance Lake.Toml.instSmartInsertTable :

SmartInsert Table

Equations

source

instance Lake.Toml.instSmartInsertArrayOfToToml {α : Type u_1} [ToToml (Array α)] :

SmartInsert (Array α)

Equations

source

instance Lake.Toml.instSmartInsertString :

SmartInsert String

Equations

source

@[inline]

def Lake.Toml.Table.insert {α : Type u_1} [enc : ToToml α] (k : Lean.Name) (v : α) (t : Table) :

Table

Inserts the encoded value into the table.

Equations

Instances For

source

@[macro_inline]

def Lake.Toml.Table.insertSome {α : Type u_1} [enc : ToToml α] (k : Lean.Name) (v? : Option α) (t : Table) :

Table

If the value is not none, inserts the encoded value into the table.

Equations

Instances For

source

instance Lake.Toml.Table.instSmartInsertOptionOfToToml {α : Type u_1} [ToToml α] :

SmartInsert (Option α)

Equations

source

@[inline]

def Lake.Toml.Table.smartInsert {α : Type u_1} [SmartInsert α] (k : Lean.Name) (v : α) (t : Table) :

Table

Insert a value into the table unless it represents a nullish value.

Equations

Instances For

source

@[macro_inline]

def Lake.Toml.Table.insertIf {α : Type u_1} [enc : ToToml α] (p : Bool) (k : Lean.Name) (v : α) (t : Table) :

Table

Insert a value into the table if p is true.

Equations

Instances For

source

@[macro_inline]

def Lake.Toml.Table.insertUnless {α : Type u_1} [enc : ToToml α] (p : Bool) (k : Lean.Name) (v : α) (t : Table) :

Table

Insert a value into the table if p is false.

Equations

Instances For

source

@[inline]

def Lake.Toml.Table.insertD {α : Type u_1} [enc : ToToml α] [BEq α] (k : Lean.Name) (v default : α) (t : Table) :

Table

Inserts the value into the table if it is not equal to default.

Equations

Instances For

Documentation

Lake.Toml.Encode

TOML Encoders #