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 : α → Nat → Std.Format
Turn a value of type
α
intoFormat
at a given precedence. The precedence value can be used to avoid parentheses if they are not necessary.
Instances
Equations
- instReprId = inferInstanceAs (Repr α)
Equations
- instReprId_1 = inferInstanceAs (Repr α)
Equations
- instReprEmpty = { reprPrec := fun (a : Empty) (a_1 : Nat) => nomatch a, a_1 }
Equations
- instReprBool = { reprPrec := fun (x : Bool) (x_1 : Nat) => match x, x_1 with | true, x => Std.Format.text "true" | false, x => Std.Format.text "false" }
Equations
- Repr.addAppParen f prec = if prec ≥ 1024 then f.paren else f
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- instReprPUnit = { reprPrec := fun (x : PUnit) (x : Nat) => Std.Format.text "PUnit.unit" }
Equations
- instReprULift = { reprPrec := fun (v : ULift α) (prec : Nat) => Repr.addAppParen (Std.Format.text "ULift.up " ++ reprArg v.down) prec }
Equations
- instReprUnit = { reprPrec := fun (x : Unit) (x : Nat) => Std.Format.text "()" }
Equations
- none.repr x = Std.Format.text "none"
- (some a).repr x = Repr.addAppParen (Std.Format.text "some " ++ reprArg a) x
Instances For
Equations
- (Sum.inl a).repr x = Repr.addAppParen (Std.Format.text "Sum.inl " ++ reprArg a) x
- (Sum.inr b).repr x = Repr.addAppParen (Std.Format.text "Sum.inr " ++ reprArg b) x
Instances For
- reprTuple : α → List Std.Format → List Std.Format
Instances
Equations
- instReprTupleOfRepr = { reprTuple := fun (a : α) (xs : List Std.Format) => repr a :: xs }
Equations
- (a, b).repr x = Std.Format.bracket "(" (Std.Format.joinSep (reprTuple b [repr a]).reverse (Std.Format.text "," ++ Std.Format.line)) ")"
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
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.toSubscriptString = n.toSubDigits.asString
Instances For
Equations
- instReprNat = { reprPrec := fun (n x : Nat) => Std.Format.text n.repr }
Equations
- instReprInt = { reprPrec := fun (i : Int) (prec : Nat) => if i < 0 then Repr.addAppParen (Std.Format.text i.repr) prec else Std.Format.text i.repr }
Equations
- hexDigitRepr n = String.singleton n.digitChar
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Char.quoteCore.smallCharToHex c = hexDigitRepr (c.toNat / 16) ++ hexDigitRepr (c.toNat % 16)
Instances For
Equations
- instReprChar = { reprPrec := fun (c : Char) (x : Nat) => Std.Format.text c.quote }
Equations
- instReprString = { reprPrec := fun (s : String) (x : Nat) => Std.Format.text s.quote }
Equations
- instReprPos = { reprPrec := fun (p : String.Pos) (x : Nat) => Std.Format.text "{ byteIdx := " ++ repr p.byteIdx ++ Std.Format.text " }" }
Equations
- instReprSubstring = { reprPrec := fun (s : Substring) (x : Nat) => Std.Format.text (s.toString.quote ++ ".toSubstring") }
Equations
- One or more equations did not get rendered due to their size.
Equations
- instReprFin n = { reprPrec := fun (f : Fin n) (x : Nat) => repr ↑f }
Equations
- instReprUInt8 = { reprPrec := fun (n : UInt8) (x : Nat) => repr n.toNat }
Equations
- instReprUInt16 = { reprPrec := fun (n : UInt16) (x : Nat) => repr n.toNat }
Equations
- instReprUInt32 = { reprPrec := fun (n : UInt32) (x : Nat) => repr n.toNat }
Equations
- instReprUInt64 = { reprPrec := fun (n : UInt64) (x : Nat) => repr n.toNat }
Equations
- instReprUSize = { reprPrec := fun (n : USize) (x : Nat) => repr n.toNat }
Equations
- [].repr n = Std.Format.text "[]"
- a.repr n = Std.Format.bracket "[" (Std.Format.joinSep a (Std.Format.text "," ++ Std.Format.line)) "]"
Instances For
Equations
- [].repr' n = Std.Format.text "[]"
- a.repr' n = Std.Format.bracketFill "[" (Std.Format.joinSep a (Std.Format.text "," ++ Std.Format.line)) "]"
Instances For
Equations
- instReprSourceInfo = { reprPrec := reprSourceInfo✝ }