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 x.toFoo.toBar into x.toBar. The 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.

The only functional difference from Lean.PrettyPrinter.Delaborator.delabProjectionApp is the walkUp function.

Instances For

    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.

    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
      def (a : A) (m : Nat) : Nat := a.n + m

      Now, x m pretty prints as m. If A is a structure, it also adds a rule that x.toA m pretty prints as m. This rule is meant to combine with the projection collapse delaborator defined in this module, where together x.toB.toA m will pretty print as 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
      def (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 b.toA 1
      -- (B.toA b).inc 1 : Int
      attribute [pp_dot] B.toA
      #check b.toA 1
      -- 1 : Int
      #check 1
      -- invalid field 'inc', the environment does not contain ''

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

      Instances For