class Printf.PrintfType (t : Type u) : Type u

• spr : String → List UPrintf → t

instance Printf.instPrintfTypeIOUnit : PrintfType (IO Unit)

Equations

• Printf.instPrintfTypeIOUnit = { spr := fun (fmt : String) (args : List Printf.UPrintf) => IO.print (Printf.uprintf fmt args.reverse) }

@[defaultInstance 1000]

instance Printf.instPrintfTypeString : PrintfType String

Equations

• Printf.instPrintfTypeString = { spr := fun (fmt : String) (args : List Printf.UPrintf) => Printf.uprintf fmt args.reverse }

instance Printf.instPrintfTypeListOfIsChar {c : Type u_1} [IsChar c] : PrintfType (List c)

Equations

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

instance Printf.instPrintfTypeForallOfPrintfArg {a : Type u_1} {r : Type u_2} [PrintfArg a] [PrintfType r] : PrintfType (a → r)

Equations

• Printf.instPrintfTypeForallOfPrintfArg = { spr := fun (fmt : String) (args : List Printf.UPrintf) (arg : a) => Printf.PrintfType.spr fmt (Printf.PrintfArg.of arg :: args) }