Documentation

Init.Data.ToString.Basic

instance instToStringIdType {α : Type u_1} [inst : ToString α] :
Equations
instance instToStringId {α : Type u_1} [inst : ToString α] :
Equations
Equations
Equations
Equations
instance instToStringDecidable {p : Prop} :
Equations
  • instToStringDecidable = { toString := fun h => match h with | isTrue h => "true" | isFalse h => "false" }
def List.toStringAux {α : Type u} [inst : ToString α] :
BoolList αString
Equations
def List.toString {α : Type u} [inst : ToString α] :
List αString
Equations
instance instToStringList {α : Type u} [inst : ToString α] :
Equations
  • instToStringList = { toString := List.toString }
Equations
instance instToStringULift {α : Type u} [inst : ToString α] :
Equations
  • instToStringULift = { toString := fun v => toString v.down }
Equations
Equations
Equations
Equations
Equations
instance instToStringFin (n : Nat) :
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
instance instToStringOption {α : Type u} [inst : ToString α] :
Equations
instance instToStringSum {α : Type u} {β : Type v} [inst : ToString α] [inst : ToString β] :
ToString (α β)
Equations
instance instToStringProd {α : Type u} {β : Type v} [inst : ToString α] [inst : ToString β] :
ToString (α × β)
Equations
instance instToStringSigma {α : Type u} {β : αType v} [inst : ToString α] [inst : (x : α) → ToString (β x)] :
Equations
  • instToStringSigma = { toString := fun x => match x with | { fst := a, snd := b } => "⟨" ++ toString a ++ ", " ++ toString b ++ "⟩" }
instance instToStringSubtype {α : Type u} {p : αProp} [inst : ToString α] :
Equations
  • instToStringSubtype = { toString := fun s => toString s.val }
def String.toInt! (s : String) :
Equations
instance instToStringExcept {ε : Type u_1} {α : Type u_2} [inst : ToString ε] [inst : ToString α] :
Equations
instance instReprExcept {ε : Type u_1} {α : Type u_2} [inst : Repr ε] [inst : Repr α] :
Repr (Except ε α)
Equations