Init.Data.Repr

source

class Repr (α : Type u) :

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 : α → Nat → Lean.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

source

@[reducible, inline]

abbrev repr {α : Type u_1} [Repr α] (a : α) :

Lean.Format

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

Equations

repr a = reprPrec a 0

source

@[reducible, inline]

abbrev reprStr {α : Type u_1} [Repr α] (a : α) :

String

Equations

reprStr a = (reprPrec a 0).pretty

source

@[reducible, inline]

abbrev reprArg {α : Type u_1} [Repr α] (a : α) :

Lean.Format

Equations

reprArg a = reprPrec a 1024

source

class ReprAtom (α : Type u) :

Type

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

source

instance instReprId {α : Type u_1} [Repr α] :

Repr (id α)

Equations

instReprId = inferInstanceAs (Repr α)

source

instance instReprId_1 {α : Type u_1} [Repr α] :

Repr (Id α)

Equations

instReprId_1 = inferInstanceAs (Repr α)

source

instance instReprEmpty :

Repr Empty

Equations

instReprEmpty = { reprPrec := fun (a : Empty) (a_1 : Nat) => nomatch a, a_1 }

source

instance instReprBool :

Repr Bool

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" }

source

def Repr.addAppParen (f : Lean.Format) (prec : Nat) :

Lean.Format

Equations

Repr.addAppParen f prec = if prec ≥ 1024 then f.paren else f

source

instance instReprDecidable {p : Prop} :

Repr (Decidable p)

Equations

One or more equations did not get rendered due to their size.

source

instance instReprPUnit :

Repr PUnit

Equations

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

source

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

Repr (ULift α)

Equations

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

source

instance instReprUnit :

Repr Unit

Equations

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

source

def Option.repr {α : Type u_1} [Repr α] :

Option α → Nat → Lean.Format

Equations

none.repr x = Std.Format.text "none"
(some a).repr x = Repr.addAppParen (Std.Format.text "some " ++ reprArg a) x

source

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

Repr (Option α)

Equations

instReprOption = { reprPrec := Option.repr }

source

def Sum.repr {α : Type u_1} {β : Type u_2} [Repr α] [Repr β] :

α ⊕ β → Nat → Lean.Format

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

source

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

Repr (α ⊕ β)

Equations

instReprSum = { reprPrec := Sum.repr }

source

class ReprTuple (α : Type u) :

Type u

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

Instances

source

instance instReprTupleOfRepr {α : Type u_1} [Repr α] :

ReprTuple α

Equations

instReprTupleOfRepr = { reprTuple := fun (a : α) (xs : List Lean.Format) => repr a :: xs }

source

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

ReprTuple (α × β)

Equations

instReprTupleProdOfRepr = { reprTuple := fun (x : α × β) (x_1 : List Lean.Format) => match x, x_1 with | (a, b), xs => reprTuple b (repr a :: xs) }

source

def Prod.repr {α : Type u_1} {β : Type u_2} [Repr α] [ReprTuple β] :

α × β → Nat → Lean.Format

Equations

(a, b).repr x = Lean.Format.bracket "(" (Lean.Format.joinSep (reprTuple b [repr a]).reverse (Std.Format.text "," ++ Lean.Format.line)) ")"

source

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

Repr (α × β)

Equations

instReprProdOfReprTuple = { reprPrec := Prod.repr }

source

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

Repr (Sigma β)

Equations

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

source

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

Repr (Subtype p)

Equations

instReprSubtype = { reprPrec := fun (s : Subtype p) (prec : Nat) => reprPrec s.val prec }

source

def Nat.digitChar (n : Nat) :

Char

Equations

One or more equations did not get rendered due to their size.

source

def Nat.toDigitsCore (base : Nat) :

Nat → Nat → List Char → List Char

Equations

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