Attributes for the pretty printer

This module defines attributes that influence pretty printer output.

opaque Lean.ppUsingAnonymousConstructorAttr : Lean.TagAttribute

opaque Lean.ppNoDotAttr : Lean.TagAttribute

def Lean.hasPPUsingAnonymousConstructorAttribute (env : Lean.Environment) (declName : Lake.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 : Lean.Environment) (declName : Lake.Name) : Bool

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

Equations

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