HepLean Documentation

Mathlib.Tactic.ProjectionNotation

Pretty printing projection notation #

Deprecated as of 2024-05-02 with Lean v4.8.0 since dot notation is now default with the introduction of pp.fieldNotation.generalized, which handles dot notation pervasively and correctly.

This module contains the @[pp_dot] attribute, which is used to configure functions to pretty print using projection notation (i.e., like x.f y rather than C.f x y).

Core's projection delaborator collapses chains of ancestor projections. For example, to turn x.toFoo.toBar into x.toBar. The pp_dot attribute works together with this delaborator to completely collapse such chains.

source
def Mathlib.ProjectionNotation.mkExtendedFieldNotationUnexpander (f : Lean.Name) :
Lean.Elab.Command.CommandElabM Unit

Given a function f that is either a true projection or a generalized projection (i.e., a function that works using extended field notation, a.k.a. "dot notation"), generates an app_unexpander for it to get it to pretty print using dot notation.

See also the docstring of the pp_dot attribute.

Equations
Instances For
    source
    def Mathlib.ProjectionNotation.ppDotAttr :
    Lean.ParserDescr

    Adding the @[pp_dot] attribute defines an app_unexpander for the given function to support pretty printing the function using extended field notation ("dot notation"). This particular attribute is only for functions whose first explicit argument is the receiver of the generalized field notation. That is to say, it is only meant for transforming C.f c x y z ... to c.f x y z ... for c : C.

    It can be used to help get projection notation to work for function-valued structure fields, since the built-in projection delaborator cannot handle excess arguments.

    Example for generalized field notation:

    structure A where
  n : Nat

@[pp_dot]
def A.foo (a : A) (m : Nat) : Nat := a.n + m

    Now, A.foo x m pretty prints as x.foo m. If A is a structure, it also adds a rule that A.foo x.toA m pretty prints as x.foo m. This rule is meant to combine with core's the projection collapse delaborator, where together A.foo x.toB.toA m will pretty print as x.foo m.

    Since the mentioned rule is a purely syntactic transformation, it might lead to output that does not round trip, though this can only occur if there exists an A-valued toA function that is not a parent projection that happens to be pretty printable using dot notation.

    Here is an example to illustrate the round tripping issue:

    import Mathlib.Tactic.ProjectionNotation

structure A where n : Int

@[pp_dot]
def A.inc (a : A) (k : Int) : Int := a.n + k

structure B where n : Nat

def B.toA (b : B) : A := ⟨b.n⟩

variable (b : B)

#check A.inc b.toA 1
-- (B.toA b).inc 1 : Int

attribute [pp_dot] B.toA
#check A.inc b.toA 1
-- b.inc 1 : Int

#check b.inc 1
-- invalid field 'inc', the environment does not contain 'B.inc'

    To avoid this, don't use pp_dot for coercion functions such as B.toA.

    Equations
    Instances For