Attributes for the pretty printer

This module defines attributes that influence pretty printer output.

opaque Lean.ppUsingAnonymousConstructorAttr : TagAttribute

Marks a structure to be pretty printed using the anonymous constructor notation (⟨a, b, c⟩).

opaque Lean.ppNoDotAttr : TagAttribute

Marks a declaration to never be pretty printed using field notation.

def Lean.hasPPUsingAnonymousConstructorAttribute (env : Environment) (declName : Name) : Bool

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

def Lean.hasPPNoDotAttribute (env : Environment) (declName : Name) : Bool

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