class Data.Default (α : Type) : Type

A class for types with a sensible default value. Unlike Inhabited, Default carries the semantic meaning of "the most commonly useful starting point". $$\text{Default}(\alpha) \Rightarrow \alpha$$

• default : α

  The default value.

@[implicit_reducible]

instance Data.instDefaultBool : Default Bool

Equations

• Data.instDefaultBool = { default := false }

@[implicit_reducible]

instance Data.instDefaultNat : Default Nat

Equations

• Data.instDefaultNat = { default := 0 }

@[implicit_reducible]

instance Data.instDefaultInt : Default Int

Equations

• Data.instDefaultInt = { default := 0 }

@[implicit_reducible]

instance Data.instDefaultString : Default String

Equations

• Data.instDefaultString = { default := "" }

@[implicit_reducible]

instance Data.instDefaultList {α : Type} : Default (List α)

Equations

• Data.instDefaultList = { default := [] }

@[implicit_reducible]

instance Data.instDefaultArray {α : Type} : Default (Array α)

Equations

• Data.instDefaultArray = { default := #[] }

@[implicit_reducible]

instance Data.instDefaultOption {α : Type} : Default (Option α)

Equations

• Data.instDefaultOption = { default := none }

@[implicit_reducible]

instance Data.instDefaultProd {α β : Type} [Default α] [Default β] : Default (α × β)

Equations

• Data.instDefaultProd = { default := (Data.Default.default, Data.Default.default) }

@[implicit_reducible]

instance Data.instDefaultUnit : Default Unit

Equations

• Data.instDefaultUnit = { default := () }