In the wake of #1910 , it has become possible to use dot notation with namespaced non-function declarations.
However, pretty printing doesn't show these terms as using dot notation.
adapting the example given for that issue:
structure Equiv (α β : Sort _) where
toFun : α → β
invFun : β → α
infixl:25 " ≃ " => Equiv
instance: CoeFun (α ≃ β) fun _ => α → β where
coe := Equiv.toFun
def Foo := Nat
def Bar := Nat
def Foo.toBar : Foo ≃ Bar := ⟨id, id⟩
variable (f : Foo)
#check f.toBar -- Foo.toBar f : Bar
ideally, the latter #check command should display f.toBar by default.
Just as dot notation improves the experience of writing and reading code, pretty printing this new instance of dot notation will allow users to more clearly see the structure of code by hiding redundant information, i.e. the namespace of the declaration.
Community Feedback
This initiative started because all porting notes referring to #1910 in mathlib came under review, and some of them mentioned that certain uses of the pp_nodot attribute were not useful yet because the dot notation wasn't available for the declarations the porting notes were referring to. See also this discussion on Zulip.
Impact
Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.
Description
In the wake of #1910 , it has become possible to use dot notation with namespaced non-function declarations. However, pretty printing doesn't show these terms as using dot notation.
adapting the example given for that issue:
ideally, the latter
#checkcommand should displayf.toBarby default.Just as dot notation improves the experience of writing and reading code, pretty printing this new instance of dot notation will allow users to more clearly see the structure of code by hiding redundant information, i.e. the namespace of the declaration.
Community Feedback
This initiative started because all porting notes referring to #1910 in mathlib came under review, and some of them mentioned that certain uses of the
pp_nodotattribute were not useful yet because the dot notation wasn't available for the declarations the porting notes were referring to. See also this discussion on Zulip.Impact
Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.