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.

Equations

• Lean.hasPPUsingAnonymousConstructorAttribute env declName = Lean.ppUsingAnonymousConstructorAttr.hasTag env declName

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

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

Equations

• Lean.hasPPNoDotAttribute env declName = Lean.ppNoDotAttr.hasTag env declName