Init.Data.Repr

instReprDecidable = { reprPrec := fun x x_1 => match x, x_1 with | isTrue x, prec => Repr.addAppParen (Std.Format.text "isTrue _") prec | isFalse x, prec => Repr.addAppParen (Std.Format.text "isFalse _") prec }

source

instance instReprPUnit :

Repr PUnit

Equations

instReprPUnit = { reprPrec := fun x x => Std.Format.text "PUnit.unit" }

source

instance instReprULift {α : Type u_1} [inst : Repr α] :

Repr (ULift α)

Equations

instReprULift = { reprPrec := fun v prec => Repr.addAppParen (Std.Format.text "ULift.up " ++ reprArg v.down) prec }

source

instance instReprUnit :

Repr Unit

Equations

instReprUnit = { reprPrec := fun v x => Std.Format.text "()" }

source

instance instReprOption {α : Type u_1} [inst : Repr α] :

Repr (Option α)

Equations

instReprOption = { reprPrec := fun x x_1 => match x, x_1 with | none, x => Std.Format.text "none" | some a, prec => Repr.addAppParen (Std.Format.text "some " ++ reprArg a) prec }

source

instance instReprSum {α : Type u_1} {β : Type u_2} [inst : Repr α] [inst : Repr β] :

Repr (α ⊕ β)

Equations

instReprSum = { reprPrec := fun x x_1 => match x, x_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 }

source

class ReprTuple (α : Type u) :

Type u

reprTuple : α → List Lean.Format → List Lean.Format

Instances

source

instance instReprTuple {α : Type u_1} [inst : Repr α] :

ReprTuple α

Equations

instReprTuple = { reprTuple := fun a xs => repr a :: xs }

source

instance instReprTupleProd {α : Type u_1} {β : Type u_2} [inst : Repr α] [inst : ReprTuple β] :

ReprTuple (α × β)

Equations

instReprTupleProd = { reprTuple := fun x x_1 => match x, x_1 with | (a, b), xs => reprTuple b (repr a :: xs) }

source

instance instReprProd {α : Type u_1} {β : Type u_2} [inst : Repr α] [inst : ReprTuple β] :

Repr (α × β)

Equations

instReprProd = { reprPrec := fun x x_1 => match x, x_1 with | (a, b), x => Lean.Format.bracket "(" (Lean.Format.joinSep (List.reverse (reprTuple b [repr a])) (Std.Format.text "," ++ Lean.Format.line)) ")" }

source

instance instReprSigma {α : Type u_1} {β : α → Type v} [inst : Repr α] [s : (x : α) → Repr (β x)] :

Repr (Sigma β)

Equations

instReprSigma = { reprPrec := fun x x_1 => match x, x_1 with | { fst := a, snd := b }, x => Lean.Format.bracket "⟨" (repr a ++ Std.Format.text ", " ++ repr b) "⟩" }

source

instance instReprSubtype {α : Type u_1} {p : α → Prop} [inst : Repr α] :

Repr (Subtype p)

Equations

instReprSubtype = { reprPrec := fun s prec => reprPrec s.val prec }

source

def Nat.digitChar (n : Nat) :

Char

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

source

def Nat.toDigitsCore (base : Nat) :

Nat → Nat → List Char → List Char

Equations

Nat.toDigitsCore base 0 x x = x
Nat.toDigitsCore base (Nat.succ fuel) x x = if x / base = 0 then Nat.digitChar (x % base) :: x else Nat.toDigitsCore base fuel (x / base) (Nat.digitChar (x % base) :: x)

source

def Nat.toDigits (base : Nat) (n : Nat) :

List Char

Equations

Nat.toDigits base n = Nat.toDigitsCore base (n + 1) n []

source

def Nat.repr (n : Nat) :

String

Equations

Nat.repr n = List.asString (Nat.toDigits 10 n)

source

def Nat.superDigitChar (n : Nat) :

Char

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

source

partial def Nat.toSuperDigitsAux :

Nat → List Char → List Char

source

def Nat.toSuperDigits (n : Nat) :

List Char

Equations

Nat.toSuperDigits n = Nat.toSuperDigitsAux n []

source

def Nat.toSuperscriptString (n : Nat) :

String

Equations

Nat.toSuperscriptString n = List.asString (Nat.toSuperDigits n)

source

instance instReprNat :

Repr Nat

Equations

instReprNat = { reprPrec := fun n x => Std.Format.text (Nat.repr n) }

source

def Int.repr :

Int → String

Equations

Int.repr x = match x with | Int.ofNat m => Nat.repr m | Int.negSucc m => "-" ++ Nat.repr (Nat.succ m)

source

instance instReprInt :

Repr Int

Equations

instReprInt = { reprPrec := fun i x => Std.Format.text (Int.repr i) }

source

def hexDigitRepr (n : Nat) :

String

Equations

hexDigitRepr n = String.singleton (Nat.digitChar n)

source

def charToHex (c : Char) :

String

Equations

charToHex c = let n := Char.toNat c; let d2 := n / 16; let d1 := n % 16; hexDigitRepr d2 ++ hexDigitRepr d1

source

def Char.quoteCore (c : Char) :

String

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

source

def Char.quote (c : Char) :

String

Equations

Char.quote c = "'" ++ Char.quoteCore c ++ "'"

source

instance instReprChar :

Repr Char

Equations

instReprChar = { reprPrec := fun c x => Std.Format.text (Char.quote c) }

source

def Char.repr (c : Char) :

String

Equations

Char.repr c = Char.quote c

source

def String.quote (s : String) :

String

Equations

String.quote s = if String.isEmpty s = true then "\"\"" else String.foldl (fun s c => s ++ Char.quoteCore c) "\"" s ++ "\""

source

instance instReprString :

Repr String

Equations

instReprString = { reprPrec := fun s x => Std.Format.text (String.quote s) }

source

instance instReprSubstring :

Repr Substring

Equations

instReprSubstring = { reprPrec := fun s x => Std.Format.text (String.quote (Substring.toString s) ++ ".toSubstring") }

source

instance instReprIterator :

Repr String.Iterator

Equations

instReprIterator = { reprPrec := fun x x_1 => match x, x_1 with | { s := s, i := pos }, prec => Repr.addAppParen (Std.Format.text "String.Iterator.mk " ++ reprArg s ++ Std.Format.text " " ++ reprArg pos) prec }

source

instance instReprFin (n : Nat) :

Repr (Fin n)

Equations

instReprFin n = { reprPrec := fun f x => repr f.val }

source

instance instReprUInt8 :

Repr UInt8

Equations

instReprUInt8 = { reprPrec := fun n x => repr (UInt8.toNat n) }

source

instance instReprUInt16 :

Repr UInt16

Equations

instReprUInt16 = { reprPrec := fun n x => repr (UInt16.toNat n) }

source

instance instReprUInt32 :

Repr UInt32

Equations

instReprUInt32 = { reprPrec := fun n x => repr (UInt32.toNat n) }

source

instance instReprUInt64 :

Repr UInt64

Equations

instReprUInt64 = { reprPrec := fun n x => repr (UInt64.toNat n) }

source

instance instReprUSize :

Repr USize

Equations

instReprUSize = { reprPrec := fun n x => repr (USize.toNat n) }

source

instance instReprList {α : Type u_1} [inst : Repr α] :

Repr (List α)

Equations

instReprList = { reprPrec := fun a n => let x := { format := repr }; match x with | x_1 => match a, n with | [], x => Std.Format.text "[]" | as, x_2 => Lean.Format.bracket "[" (Lean.Format.joinSep as (Std.Format.text "," ++ Lean.Format.line)) "]" }

source

instance instReprList_1 {α : Type u_1} [inst : Repr α] [inst : ReprAtom α] :

Repr (List α)

Equations

instReprList_1 = { reprPrec := fun a n => let x := { format := repr }; match x with | x_1 => match a, n with | [], x => Std.Format.text "[]" | as, x_2 => Std.Format.bracketFill "[" (Lean.Format.joinSep as (Std.Format.text "," ++ Lean.Format.line)) "]" }