Documentation

Lean.PrettyPrinter.Delaborator.Attributes

Attributes for the pretty printer #

This module defines attributes that influence pretty printer output.

Returns whether or not the given declaration has the @[pp_using_anonymous_constructor] attribute.

Equations

Returns whether or not the given declaration has the @[pp_nodot] attribute.

Equations