@[instance 100]
Equations
Formats an optional value, with no expectation that the Lean parser should be able to parse the result.
This function is usually accessed through the ToFormat (Option α)
instance.
Equations
Instances For
instance
instToFormatProd
{α : Type u}
{β : Type v}
[Std.ToFormat α]
[Std.ToFormat β]
:
Std.ToFormat (α × β)
Equations
Converts a string to a pretty-printer document, replacing newlines in the string with
Std.Format.line
.