# 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.

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

- One or more equations did not get rendered due to their size.

## Instances For

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

- Mathlib.ProjectionNotation.ppDotAttr = Lean.ParserDescr.node `Mathlib.ProjectionNotation.ppDotAttr 1024 (Lean.ParserDescr.nonReservedSymbol "pp_dot" false)