HepLean Documentation

Init.Data.ToString.Basic

class ToString (α : Type u) :
Instances
    instance instToStringId {α : Type u_1} [ToString α] :
    Equations
    instance instToStringId_1 {α : Type u_1} [ToString α] :
    Equations
    Equations
    Equations
    Equations
    Equations
    Equations
    • instToStringDecidable = { toString := fun (h : Decidable p) => match h with | isTrue h => "true" | isFalse h => "false" }
    def List.toString {α : Type u_1} [ToString α] :
    List αString
    Equations
    Instances For
      instance instToStringList {α : Type u} [ToString α] :
      Equations
      • instToStringList = { toString := List.toString }
      Equations
      instance instToStringULift {α : Type u} [ToString α] :
      Equations
      • instToStringULift = { toString := fun (v : ULift α) => toString v.down }
      Equations
      Equations
      Equations
      Equations
      Equations
      instance instToStringFin (n : Nat) :
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Instances For
        instance instToStringOption {α : Type u} [ToString α] :
        Equations
        instance instToStringSum {α : Type u} {β : Type v} [ToString α] [ToString β] :
        ToString (α β)
        Equations
        • One or more equations did not get rendered due to their size.
        instance instToStringProd {α : Type u} {β : Type v} [ToString α] [ToString β] :
        ToString (α × β)
        Equations
        instance instToStringSigma {α : Type u} {β : αType v} [ToString α] [(x : α) → ToString (β x)] :
        Equations
        instance instToStringSubtype {α : Type u} {p : αProp} [ToString α] :
        Equations
        Equations
        Instances For
          Equations
          • s.isInt = if s.get 0 = '-' then (s.toSubstring.drop 1).isNat else s.isNat
          Instances For
            Equations
            • s.toInt! = match s.toInt? with | some v => v | none => panic "Int expected"
            Instances For
              instance instToStringExcept {ε : Type u_1} {α : Type u_2} [ToString ε] [ToString α] :
              Equations
              instance instReprExcept {ε : Type u_1} {α : Type u_2} [Repr ε] [Repr α] :
              Repr (Except ε α)
              Equations
              • One or more equations did not get rendered due to their size.