Documentation

Init.Data.Repr

class Repr (α : Type u) :

A typeclass that specifies the standard way of turning values of some type into Format.

When rendered this Format should be as close as possible to something that can be parsed as the input value.

  • reprPrec : αNatLean.Format

    Turn a value of type α into Format at a given precedence. The precedence value can be used to avoid parentheses if they are not necessary.

Instances
    @[reducible, inline]
    abbrev repr {α : Type u_1} [Repr α] (a : α) :

    Turn a into Format using its Repr instance. The precedence level is initially set to 0.

    Equations
    Instances For
      @[reducible, inline]
      abbrev reprStr {α : Type u_1} [Repr α] (a : α) :
      Equations
      Instances For
        @[reducible, inline]
        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 instReprId {α : Type u_1} [Repr α] :
              Repr (id α)
              Equations
              instance instReprId_1 {α : 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 instReprTupleOfRepr {α : Type u_1} [Repr α] :
                      Equations
                      instance instReprTupleProdOfRepr {α : Type u_1} {β : Type u_2} [Repr α] [ReprTuple β] :
                      ReprTuple (α × β)
                      Equations
                      def Prod.repr {α : Type u_1} {β : Type u_2} [Repr α] [ReprTuple β] :
                      α × βNatLean.Format
                      Equations
                      Instances For
                        instance instReprProdOfReprTuple {α : Type u_1} {β : Type u_2} [Repr α] [ReprTuple β] :
                        Repr (α × β)
                        Equations
                        • instReprProdOfReprTuple = { reprPrec := Prod.repr }
                        instance instReprSigma {α : Type u_1} {β : αType v} [Repr α] [(x : α) → Repr (β x)] :
                        Repr (Sigma β)
                        Equations
                        instance instReprSubtype {α : Type u_1} {p : αProp} [Repr α] :
                        Equations
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def Nat.toDigitsCore (base : Nat) :
                          NatNatList CharList Char
                          Equations
                          • base.toDigitsCore 0 x✝ x = x
                          • base.toDigitsCore fuel.succ x✝ x = let d := (x✝ % base).digitChar; let n' := x✝ / base; if n' = 0 then d :: x else base.toDigitsCore fuel n' (d :: x)
                          Instances For
                            def Nat.toDigits (base : Nat) (n : Nat) :
                            Equations
                            • base.toDigits n = base.toDigitsCore (n + 1) n []
                            Instances For
                              @[extern lean_string_of_usize]
                              Equations
                              Instances For
                                @[implemented_by _private.Init.Data.Repr.0.Nat.reprFast]
                                def Nat.repr (n : Nat) :
                                Equations
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    • n.toSuperDigits = n.toSuperDigitsAux []
                                    Instances For
                                      Equations
                                      • n.toSuperscriptString = n.toSuperDigits.asString
                                      Instances For
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          Equations
                                          • n.toSubDigits = n.toSubDigitsAux []
                                          Instances For
                                            Equations
                                            • n.toSubscriptString = n.toSubDigits.asString
                                            Instances For
                                              instance instReprNat :
                                              Equations
                                              Equations
                                              Instances For
                                                instance instReprInt :
                                                Equations
                                                Equations
                                                Instances For
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    Equations
                                                    Instances For
                                                      Equations
                                                      • c.quote = "'" ++ c.quoteCore ++ "'"
                                                      Instances For
                                                        Equations
                                                        def Char.repr (c : Char) :
                                                        Equations
                                                        • c.repr = c.quote
                                                        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 instReprListOfReprAtom {α : Type u_1} [Repr α] [ReprAtom α] :
                                                                Repr (List α)
                                                                Equations
                                                                • instReprListOfReprAtom = { reprPrec := List.repr' }