def Std.Format.paren' (p : Nat → Bool) (f : Format) (prec : Nat) : Format

Equations

• Std.Format.paren' p f prec = bif p prec then f.paren else f

def Std.Format.infixl {α : Type u} (f : α → Nat → Format) (p_op : Nat) (op : String) (x y : α) : Nat → Format

Equations

• Std.Format.infixl f p_op op x y = Std.Format.paren' (fun (x : Nat) => decide (x > p_op)) (f x p_op ++ Std.Format.text " " ++ Std.Format.text op ++ Std.Format.text " " ++ f y (p_op + 1))

def Std.Format.infixr {α : Type u} (f : α → Nat → Format) (p_op : Nat) (op : String) (x y : α) : Nat → Format

Equations

• Std.Format.infixr f p_op op x y = Std.Format.paren' (fun (x : Nat) => decide (x > p_op)) (f x (p_op + 1) ++ Std.Format.text " " ++ Std.Format.text op ++ Std.Format.text " " ++ f y p_op)

def Std.Format.infix {α : Type u} (f : α → Nat → Format) (p_op : Nat) (op : String) (x y : α) : Nat → Format

Equations

• Std.Format.infix f p_op op x y = Std.Format.paren' (fun (x : Nat) => decide (x > p_op)) (f x p_op ++ Std.Format.text " " ++ Std.Format.text op ++ Std.Format.text " " ++ f y p_op)

def Std.Format.prefix {α : Type u} (f : α → Nat → Format) (p_op : Nat) (op : String) (x : α) : Nat → Format

Equations

• Std.Format.prefix f p_op op x = Std.Format.paren' (fun (x : Nat) => decide (x > p_op)) (Std.Format.text op ++ f x p_op)

def Std.Format.postfix {α : Type u} (f : α → Nat → Format) (p_op : Nat) (op : String) (x : α) : Nat → Format

Equations

• Std.Format.postfix f p_op op x = Std.Format.paren' (fun (x : Nat) => decide (x > p_op)) (f x p_op ++ Std.Format.text op)

def Std.Format.binder {α : Type u} (f : α → Nat → Format) (p_op : Nat) (p1 x p2 : String) (dom : α) (p3 : String) (pred : α) (p4 : String) : Nat → Format

Equations

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

def Std.Format.binder' {α : Type u} {β : Type v} (f : α → Nat → Format) (f' : β → Nat → Format) (p_op : Nat) (p1 x p2 : String) (dom : α) (p3 : String) (pred : β) (p4 : String) : Nat → Format

Equations

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

def Std.Format.indent (n : Int) (f : Format) : Format

Equations

• Std.Format.indent n f = Std.Format.nest n (Std.Format.line ++ f)

@[inline]

def Std.Format.cbracket (f : Format) : Format

Curly brackets.

Equations

• f.cbracket = Std.Format.bracket "{" f "}"