Attributes for the pretty printer

This module defines attributes that influence pretty printer output.

opaque Lean.ppUsingAnonymousConstructorAttr : TagAttribute

opaque Lean.ppNoDotAttr : TagAttribute

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