dot notation printer

Stream: lean4

[Kenny Lau]

axiom Nat.fib : Nat → Nat

variable (n : Nat)

#check Nat.fib n -- n.fib
#check (3 : Nat).fib -- Nat.fib 3

I've noticed that sometimes pp uses dot notation and sometimes it doesn't. What is the exact rule? I can't quite figure it out from my usecases.

[Damiano Testa]

My not-so-fleshed-out rule is that it tries to round trip, without using type ascriptions.

[Damiano Testa]

That at least works in the case above!

[Kenny Lau]

@Damiano Testa the real testcase (with import Mathlib) that I'm facing is:

import Mathlib

notation:max 𝒜"₊" => HomogeneousIdeal.irrelevant 𝒜

variable {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι]
  [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ)
  [GradedRing 𝒜]

axiom HomogeneousIdeal.map :  HomogeneousIdeal 𝒜 → HomogeneousIdeal 𝒜

#check 𝒜₊.map 𝒜 -- HomogeneousIdeal.map 𝒜 𝒜₊

axiom Nat.foo : Nat → Int → Nat
variable (n : Nat)

#check n.foo 3

[Kenny Lau]

where the first #check fails to use dot notation

[Kenny Lau]

(and it isn't because of the notation, you can delete that line)

[Kenny Lau]

ah... I think it might be because the pp tries to check map and found Ideal.map as well??

[Kenny Lau]

so I.map wouldn't be unambiguous

[Kyle Miller]

Nat.fib 3 doesn't pretty print as 3.fib because numerals are special cased (it never uses dot notation for numerals). It's unlikely to round trip. Worse, 3.fib doesn't even parse.

The reason HomogeneousIdeal.map doesn't pretty print with dot notation is that the pretty printer uses the heuristic that it should only use dot notation if the first explicit argument is the "object" of dot notation.

It's not sophisticated enough yet to actually check whether there is an ambiguity with map in other namespaces.

[Kenny Lau]

aha! somehow i never noticed maybe, thanks for the (obvious in hindsight) explanation!

axiom Nat.fib : Int → Nat → Nat

variable (m : Int) (n : Nat)
#check n.fib m -- Nat.fib m n