- reprPrec : α → Nat → Std.Format
Instances
- IO.FS.instReprMetadata
- instReprUInt32
- Lean.Meta.Simp.instReprConfig
- instReprUInt8
- instReprSubstring
- instReprStdGen
- IO.FS.instReprFileType
- instReprSigma
- instReprSourceInfo
- EStateM.instReprResult
- instReprId
- instReprDecidable
- instReprSubtype
- IO.FS.instReprSystemTime
- instReprPUnit
- instReprUnit
- instReprOption
- Lean.Name.instReprSyntax
- instReprUInt64
- IO.FS.instReprDirEntry
- Lean.Meta.instReprEtaStructMode
- instReprUInt16
- Lean.Meta.DSimp.instReprConfig
- Lean.Data.AC.instReprExpr
- instReprIterator
- instReprList
- instReprList_1
- instReprSubarray
- instReprSum
- instReprFloat
- instReprNat
- Lean.Meta.instReprTransparencyMode
- Array.instReprArray
- instReprProd
- System.instReprFilePath
- instReprULift
- instReprBool
- instReprIdType
- instReprExcept
- instReprPos
- Lean.Name.instReprName
- instReprString
- instReprUSize
- instReprChar
- instReprFin
- instReprInt
Equations
- instReprIdType = inferInstanceAs (Repr α)
Equations
- instReprId = inferInstanceAs (Repr α)
Equations
- instReprBool = { reprPrec := fun _fun_discr _fun_discr_1 => match _fun_discr, _fun_discr_1 with | true, x => Std.Format.text "true" | false, x => Std.Format.text "false" }
Equations
- Repr.addAppParen f prec = if prec ≥ 1024 then Std.Format.paren f else f
Equations
- instReprDecidable = { reprPrec := fun _fun_discr _fun_discr_1 => match _fun_discr, _fun_discr_1 with | isTrue h, prec => Repr.addAppParen (Std.Format.text "isTrue _") prec | isFalse h, prec => Repr.addAppParen (Std.Format.text "isFalse _") prec }
Equations
- instReprPUnit = { reprPrec := fun x x => Std.Format.text "PUnit.unit" }
Equations
- instReprULift = { reprPrec := fun v prec => Repr.addAppParen (Std.Format.text "ULift.up " ++ reprArg v.down) prec }
Equations
- instReprUnit = { reprPrec := fun x x => Std.Format.text "()" }
Equations
- instReprOption = { reprPrec := fun _fun_discr _fun_discr_1 => match _fun_discr, _fun_discr_1 with | none, x => Std.Format.text "none" | some a, prec => Repr.addAppParen (Std.Format.text "some " ++ reprArg a) prec }
Equations
- instReprSum = { reprPrec := fun _fun_discr _fun_discr_1 => match _fun_discr, _fun_discr_1 with | Sum.inl a, prec => Repr.addAppParen (Std.Format.text "Sum.inl " ++ reprArg a) prec | Sum.inr b, prec => Repr.addAppParen (Std.Format.text "Sum.inr " ++ reprArg b) prec }
- reprTuple : α → List Std.Format → List Std.Format
Instances
Equations
- instReprProd = { reprPrec := fun _fun_discr _fun_discr_1 => match _fun_discr, _fun_discr_1 with | (a, b), x => Std.Format.bracket "(" (Std.Format.joinSep (List.reverse (reprTuple b [repr a])) (Std.Format.text "," ++ Std.Format.line)) ")" }
instance
instReprSigma
{α : Type u_1}
{β : α → Type v}
[inst : Repr α]
[inst : (x : α) → Repr (β x)]
:
Equations
- instReprSigma = { reprPrec := fun _fun_discr _fun_discr_1 => match _fun_discr, _fun_discr_1 with | { fst := a, snd := b }, x => Std.Format.bracket "⟨" (repr a ++ Std.Format.text ", " ++ repr b) "⟩" }
Equations
- Nat.digitChar n = if n = 0 then Char.ofNat 48 else if n = 1 then Char.ofNat 49 else if n = 2 then Char.ofNat 50 else if n = 3 then Char.ofNat 51 else if n = 4 then Char.ofNat 52 else if n = 5 then Char.ofNat 53 else if n = 6 then Char.ofNat 54 else if n = 7 then Char.ofNat 55 else if n = 8 then Char.ofNat 56 else if n = 9 then Char.ofNat 57 else if n = 10 then Char.ofNat 97 else if n = 11 then Char.ofNat 98 else if n = 12 then Char.ofNat 99 else if n = 13 then Char.ofNat 100 else if n = 14 then Char.ofNat 101 else if n = 15 then Char.ofNat 102 else Char.ofNat 42
Equations
- Nat.toDigitsCore base 0 _fun_discr _fun_discr = _fun_discr
- Nat.toDigitsCore base (Nat.succ fuel) _fun_discr _fun_discr = if _fun_discr / base = 0 then Nat.digitChar (_fun_discr % base) :: _fun_discr else Nat.toDigitsCore base fuel (_fun_discr / base) (Nat.digitChar (_fun_discr % base) :: _fun_discr)
Equations
- Nat.toDigits base n = Nat.toDigitsCore base (n + 1) n []
Equations
- Nat.superDigitChar n = if n = 0 then Char.ofNat 8304 else if n = 1 then Char.ofNat 185 else if n = 2 then Char.ofNat 178 else if n = 3 then Char.ofNat 179 else if n = 4 then Char.ofNat 8308 else if n = 5 then Char.ofNat 8309 else if n = 6 then Char.ofNat 8310 else if n = 7 then Char.ofNat 8311 else if n = 8 then Char.ofNat 8312 else if n = 9 then Char.ofNat 8313 else Char.ofNat 42
Equations
Equations
Equations
- instReprNat = { reprPrec := fun n x => Std.Format.text (Nat.repr n) }
Equations
- instReprInt = { reprPrec := fun i x => Std.Format.text (Int.repr i) }
Equations
Equations
- charToHex c = let n := Char.toNat c; let d2 := n / 16; let d1 := n % 16; hexDigitRepr d2 ++ hexDigitRepr d1
Equations
- Char.quoteCore c = if c = Char.ofNat 10 then "\\n" else if c = Char.ofNat 9 then "\\t" else if c = Char.ofNat 92 then "\\\\" else if c = Char.ofNat 34 then "\\\"" else if Char.toNat c ≤ 31 ∨ c = Char.ofNat 127 then "\\x" ++ charToHex c else String.singleton c
Equations
- instReprChar = { reprPrec := fun c x => Std.Format.text (Char.quote c) }
Equations
- String.quote s = if String.isEmpty s = true then "\"\"" else String.foldl (fun s c => s ++ Char.quoteCore c) "\"" s ++ "\""
Equations
- instReprString = { reprPrec := fun s x => Std.Format.text (String.quote s) }
Equations
- instReprPos = { reprPrec := fun p x => Std.Format.text "{ byteIdx := " ++ repr p.byteIdx ++ Std.Format.text " }" }
Equations
- instReprSubstring = { reprPrec := fun s x => Std.Format.text (String.quote (Substring.toString s) ++ ".toSubstring") }
Equations
- instReprIterator = { reprPrec := fun _fun_discr _fun_discr_1 => match _fun_discr, _fun_discr_1 with | { s := s, i := pos }, prec => Repr.addAppParen (Std.Format.text "String.Iterator.mk " ++ reprArg s ++ Std.Format.text " " ++ reprArg pos) prec }
Equations
- instReprFin n = { reprPrec := fun f x => repr f.val }
Equations
- instReprUInt8 = { reprPrec := fun n x => repr (UInt8.toNat n) }
Equations
- instReprUInt16 = { reprPrec := fun n x => repr (UInt16.toNat n) }
Equations
- instReprUInt32 = { reprPrec := fun n x => repr (UInt32.toNat n) }
Equations
- instReprUInt64 = { reprPrec := fun n x => repr (UInt64.toNat n) }
Equations
- instReprUSize = { reprPrec := fun n x => repr (USize.toNat n) }
Equations
- instReprList = { reprPrec := fun a n => let _ := { format := repr }; match a, n with | [], x => Std.Format.text "[]" | as, x => Std.Format.bracket "[" (Std.Format.joinSep as (Std.Format.text "," ++ Std.Format.line)) "]" }
Equations
- instReprList_1 = { reprPrec := fun a n => let _ := { format := repr }; match a, n with | [], x => Std.Format.text "[]" | as, x => Std.Format.bracketFill "[" (Std.Format.joinSep as (Std.Format.text "," ++ Std.Format.line)) "]" }
Equations
- instReprSourceInfo = { reprPrec := [anonymous] }