Pretty printing projection notation #
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).
This module also contains a delaborator for collapsing chains of ancestor projections.
For example, to turn
pp_dot attribute works together
with this attribute to completely collapse such chains.
Like the projection delaborator from core Lean, but collapses projections to parent structures into a single projection.
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
app_unexpander for it to get it to pretty print using dot notation.
See also the docstring of 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
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:
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
the projection collapse delaborator defined in this module, where together
A.foo x.toB.toA m
will pretty print as
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
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