Documentation

Mathlib.Tactic.ProjectionNotation

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.

source
opaque Mathlib.ProjectionNotation.pp.collapseStructureProjections :
Lean.Option Bool
source
def Mathlib.ProjectionNotation.getPPCollapseStructureProjections (o : Lean.Options) :
Bool
Equations
Instances For
    source
    def Mathlib.ProjectionNotation.delabProjectionApp' :
    Lean.PrettyPrinter.Delaborator.Delab

    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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      partial def Mathlib.ProjectionNotation.delabProjectionApp'.walkUp (env : Lean.Environment) {α : Type} (done : Lean.PrettyPrinter.Delaborator.DelabM α) :
      Lean.PrettyPrinter.Delaborator.DelabM α
      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
      • One or more equations did not get rendered due to their size.
      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 the projection collapse delaborator defined in this module, 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