Documentation

Init.Data.Repr

class Repr (α : Type u) :
Instances
    @[inline, reducible]
    abbrev repr {α : Type u_1} [Repr α] (a : α) :
    Equations
    Instances For
      @[inline, reducible]
      abbrev reprStr {α : Type u_1} [Repr α] (a : α) :
      Equations
      Instances For
        @[inline, reducible]
        abbrev reprArg {α : Type u_1} [Repr α] (a : α) :
        Equations
        Instances For
          class ReprAtom (α : Type u) :

            Auxiliary class for marking types that should be considered atomic by Repr methods. We use it at Repr (List α) to decide whether bracketFill should be used or not.

            Instances
              instance instReprIdType {α : Type u_1} [Repr α] :
              Repr (id α)
              Equations
              instance instReprId {α : Type u_1} [Repr α] :
              Repr (Id α)
              Equations
              Equations
              Equations
              Instances For
                instance instReprDecidable {p : Prop} :
                Equations
                • One or more equations did not get rendered due to their size.
                Equations
                instance instReprULift {α : Type u_1} [Repr α] :
                Repr (ULift α)
                Equations
                Equations
                def Option.repr {α : Type u_1} [Repr α] :
                Equations
                Instances For
                  instance instReprOption {α : Type u_1} [Repr α] :
                  Equations
                  • instReprOption = { reprPrec := Option.repr }
                  def Sum.repr {α : Type u_1} {β : Type u_2} [Repr α] [Repr β] :
                  α βNatLean.Format
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    instance instReprSum {α : Type u_1} {β : Type u_2} [Repr α] [Repr β] :
                    Repr (α β)
                    Equations
                    • instReprSum = { reprPrec := Sum.repr }
                    class ReprTuple (α : Type u) :
                    Instances
                      instance instReprTuple {α : Type u_1} [Repr α] :
                      Equations
                      • instReprTuple = { reprTuple := fun a xs => repr a :: xs }
                      instance instReprTupleProd {α : Type u_1} {β : Type u_2} [Repr α] [ReprTuple β] :
                      ReprTuple (α × β)
                      Equations
                      • instReprTupleProd = { reprTuple := fun x x_1 => match x, x_1 with | (a, b), xs => reprTuple b (repr a :: xs) }
                      def Prod.repr {α : Type u_1} {β : Type u_2} [Repr α] [ReprTuple β] :
                      α × βNatLean.Format
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        instance instReprProd {α : Type u_1} {β : Type u_2} [Repr α] [ReprTuple β] :
                        Repr (α × β)
                        Equations
                        • instReprProd = { reprPrec := Prod.repr }
                        instance instReprSigma {α : Type u_1} {β : αType v} [Repr α] [(x : α) → Repr (β x)] :
                        Repr (Sigma β)
                        Equations
                        • One or more equations did not get rendered due to their size.
                        instance instReprSubtype {α : Type u_1} {p : αProp} [Repr α] :
                        Equations
                        • instReprSubtype = { reprPrec := fun s prec => reprPrec s.val prec }
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def Nat.toDigitsCore (base : Nat) :
                          NatNatList CharList Char
                          Equations
                          Instances For
                            def Nat.toDigits (base : Nat) (n : Nat) :
                            Equations
                            Instances For
                              def Nat.repr (n : Nat) :
                              Equations
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  instance instReprNat :
                                  Equations
                                  Equations
                                  Instances For
                                    instance instReprInt :
                                    Equations
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      Instances For
                                        Equations
                                        Instances For
                                          Equations
                                          def Char.repr (c : Char) :
                                          Equations
                                          Instances For
                                            Equations
                                            Instances For
                                              Equations
                                              Equations
                                              Equations
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              instance instReprFin (n : Nat) :
                                              Repr (Fin n)
                                              Equations
                                              Equations
                                              Equations
                                              Equations
                                              Equations
                                              Equations
                                              def List.repr {α : Type u_1} [Repr α] (a : List α) (n : Nat) :
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                instance instReprList {α : Type u_1} [Repr α] :
                                                Repr (List α)
                                                Equations
                                                • instReprList = { reprPrec := List.repr }
                                                def List.repr' {α : Type u_1} [Repr α] [ReprAtom α] (a : List α) (n : Nat) :
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  instance instReprList_1 {α : Type u_1} [Repr α] [ReprAtom α] :
                                                  Repr (List α)
                                                  Equations
                                                  • instReprList_1 = { reprPrec := List.repr' }