Init.Data.Format.Basic

source

inductive Std.Format.FlattenBehavior:

Type

allOrNone: Std.Format.FlattenBehavior
fill: Std.Format.FlattenBehavior

source

instance Std.Format.instInhabitedFlattenBehavior:

Inhabited Std.Format.FlattenBehavior

Equations

Std.Format.instInhabitedFlattenBehavior = { default := Std.Format.FlattenBehavior.allOrNone }

source

instance Std.Format.instBEqFlattenBehavior:

BEq Std.Format.FlattenBehavior

Equations

Std.Format.instBEqFlattenBehavior = { beq := [anonymous] }

source

inductive Std.Format:

Type

nil: Lean.Format
line: Lean.Format
text: String → Lean.Format
nest: Int → Lean.Format → Lean.Format
append: Lean.Format → Lean.Format → Lean.Format
group: Lean.Format → optParam Std.Format.FlattenBehavior Std.Format.FlattenBehavior.allOrNone → Lean.Format
tag: Nat → Lean.Format → Lean.Format

source

instance Std.instInhabitedFormat:

Inhabited Lean.Format

Equations

Std.instInhabitedFormat = { default := Lean.Format.nil }

source

def Std.Format.isEmpty:

Lean.Format → Bool

Equations

Std.Format.isEmpty Lean.Format.nil = true
Std.Format.isEmpty Lean.Format.line = false
Std.Format.isEmpty (Std.Format.text msg) = (msg == "")
Std.Format.isEmpty (Lean.Format.nest indent f) = Std.Format.isEmpty f
Std.Format.isEmpty (Std.Format.append f₁ f₂) = (Std.Format.isEmpty f₁ && Std.Format.isEmpty f₂)
Std.Format.isEmpty (Lean.Format.group f behavior) = Std.Format.isEmpty f
Std.Format.isEmpty (Lean.Format.tag a f) = Std.Format.isEmpty f

source

def Std.Format.fill (f : Lean.Format) :

Lean.Format

Equations

Lean.Format.fill f = Lean.Format.group f Std.Format.FlattenBehavior.fill

source

@[export lean_format_append]

def Std.Format.appendEx (a : Lean.Format) (b : Lean.Format) :

Lean.Format

Equations

Std.Format.appendEx a b = Std.Format.append a b

source

@[export lean_format_group]

def Std.Format.groupEx:

Lean.Format → Lean.Format

Equations

Std.Format.groupEx a = Lean.Format.group a

source

instance Std.Format.instAppendFormat:

Append Lean.Format

Equations

Std.Format.instAppendFormat = { append := Std.Format.append }

source

instance Std.Format.instCoeStringFormat:

Coe String Lean.Format

Equations

Std.Format.instCoeStringFormat = { coe := Std.Format.text }

source

def Std.Format.join (xs : List Lean.Format) :

Lean.Format

Equations

Lean.Format.join xs = List.foldl (fun a a_1 => a ++ a_1) (Std.Format.text "") xs

source

def Std.Format.isNil:

Lean.Format → Bool

Equations

Std.Format.isNil _fun_discr = match _fun_discr with | Lean.Format.nil => true | x => false

source

instance Std.Format.instInhabitedSpaceResult:

Inhabited Std.Format.SpaceResult

Equations

Std.Format.instInhabitedSpaceResult = { default := { foundLine := default, foundFlattenedHardLine := default, space := default } }

source

class Std.Format.MonadPrettyFormat (m : Type → Type) :

Type

pushOutput : String → m Unit
pushNewline : Nat → m Unit
currColumn : m Nat
Start a scope tagged with n.
startTag : Nat → m Unit
Exit the scope of n-many opened tags.
endTags : Nat → m Unit

A monad in which we can pretty-print Format objects.

Instances

source

def Std.Format.prettyM {m : Type → Type} (f : Lean.Format) (w : Nat) (indent : optParam Nat 0) [inst : Monad m] [inst : Std.Format.MonadPrettyFormat m] :

m Unit

Equations

Std.Format.prettyM f w indent = Std.Format.be w [{ flatten := false, flb := Std.Format.FlattenBehavior.allOrNone, items := [{ f := f, indent := Int.ofNat indent, activeTags := 0 }] }]

source

@[inline]

def Std.Format.bracket (l : String) (f : Lean.Format) (r : String) :

Lean.Format

Equations

Lean.Format.bracket l f r = Lean.Format.group (Lean.Format.nest (Int.ofNat (String.length l)) (Std.Format.text l ++ f ++ Std.Format.text r))

source

@[inline]

def Std.Format.paren (f : Lean.Format) :

Lean.Format

Equations

Lean.Format.paren f = Lean.Format.bracket "(" f ")"

source

@[inline]

def Std.Format.sbracket (f : Lean.Format) :

Lean.Format

Equations

Lean.Format.sbracket f = Lean.Format.bracket "[" f "]"

source

@[inline]

def Std.Format.bracketFill (l : String) (f : Lean.Format) (r : String) :

Lean.Format

Equations

Std.Format.bracketFill l f r = Lean.Format.fill (Lean.Format.nest (Int.ofNat (String.length l)) (Std.Format.text l ++ f ++ Std.Format.text r))

source

def Std.Format.defIndent:

Nat

Equations

Std.Format.defIndent = 2

source

def Std.Format.defUnicode:

Bool

Equations

Std.Format.defUnicode = true

source

def Std.Format.defWidth:

Nat

Equations

Std.Format.defWidth = 120

source

def Std.Format.nestD (f : Lean.Format) :

Lean.Format

Equations

Std.Format.nestD f = Lean.Format.nest (Int.ofNat Std.Format.defIndent) f

source

def Std.Format.indentD (f : Lean.Format) :

Lean.Format

Equations

Std.Format.indentD f = Std.Format.nestD (Lean.Format.line ++ f)

source

instance Std.Format.instMonadPrettyFormatStateMState:

Std.Format.MonadPrettyFormat (StateM Std.Format.State)

Equations

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

source

@[export lean_format_pretty]

def Std.Format.pretty (f : Lean.Format) (w : optParam Nat Std.Format.defWidth) :

String

Pretty-print a Format object as a string with expected width w.

Equations

Lean.Format.pretty f w = let act := Std.Format.prettyM f w 0; (act { out := "", column := 0 }).snd.out

source

class Std.ToFormat (α : Type u) :

Type u

format : α → Lean.Format

Instances

source

instance Std.instToFormatFormat:

Lean.ToFormat Lean.Format

Equations

Std.instToFormatFormat = { format := fun f => f }

source

instance Std.instToFormatString:

Lean.ToFormat String

Equations

Std.instToFormatString = { format := fun s => Std.Format.text s }

source

def Std.Format.joinSep {α : Type u} [inst : Lean.ToFormat α] :

List α → Lean.Format → Lean.Format

Equations

Lean.Format.joinSep [] _fun_discr = Lean.Format.nil
Lean.Format.joinSep [a] _fun_discr = Lean.format a
Lean.Format.joinSep (a :: as) _fun_discr = Lean.format a ++ _fun_discr ++ Lean.Format.joinSep as _fun_discr

source

def Std.Format.prefixJoin {α : Type u} [inst : Lean.ToFormat α] (pre : Lean.Format) :

List α → Lean.Format

Equations

Std.Format.prefixJoin pre [] = Lean.Format.nil
Std.Format.prefixJoin pre (a :: as) = pre ++ Lean.format a ++ Std.Format.prefixJoin pre as

source

def Std.Format.joinSuffix {α : Type u} [inst : Lean.ToFormat α] :

List α → Lean.Format → Lean.Format

Equations

Std.Format.joinSuffix [] _fun_discr = Lean.Format.nil
Std.Format.joinSuffix (a :: as) _fun_discr = Lean.format a ++ _fun_discr ++ Std.Format.joinSuffix as _fun_discr