Documentation

Std.Lean.Delaborator

Pretty print a const expression using delabConst and generate terminfo. This function avoids inserting @ if the constant is for a function whose first argument is implicit, which is what the default toMessageData for Expr does. Panics if e is not a constant.

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