pretty printer uses projection notation only for first arg

Stream: general

[Kenny Lau]

def foo := ℕ
def foo.L (x : foo) (y : ℕ) := 0
def foo.R (x : ℕ) (y : foo) := 0
def bar : foo := (0 : ℕ)

example : bar.L 0 = bar.R 0 :=
by skip

/-
tactic failed, there are unsolved goals
state:
⊢ bar.L 0 = foo.R 0 bar
-/

[Kenny Lau]

the pretty printer uses projection notation bar.L 0 instead of foo.L bar 0 if the first argument is of type foo

[Kenny Lau]

but not for the second argument (e.g. foo.R 0 bar)

[Kenny Lau]

is this the intended behaviour?

[Kenny Lau]

also, I remember that a few weeks ago this feature didn't exist, that the pretty printer would not use projection notation at all: does this mean projection notation is now encouraged?

[Kevin Buzzard]

I was just faced with the goal 3.prime. I'm still getting used to the new way

[Mario Carneiro]

I think it is good that it doesn't flip arguments. Note that you can get some very weird results when other arguments are "accidentally" of the right type:

def nat.case {α} (a b : α) (n : ℕ) : α := nat.cases_on n a (λ _, b)

variables (a b c : ℕ)
#check nat.case a b c -- a.case b c : ℕ
#check a.case b c -- b.case c a : ℕ

[Mario Carneiro]

Here's another fun one:

example {p} (h : p) : p ∨ p ∨ p := (or.inr h).inr

[Shing Tak Lam]

Mario Carneiro said:

I think it is good that it doesn't flip arguments. Note that you can get some very weird results when other arguments are "accidentally" of the right type:

def nat.case {α} (a b : α) (n : ℕ) : α := nat.cases_on n a (λ _, b)

variables (a b c : ℕ)
#check nat.case a b c -- a.case b c : ℕ
#check a.case b c -- b.case c a : ℕ

That kind of breaks extract_goal...

import tactic

def nat.case {α} (a b : α) (n : ℕ) : α := nat.cases_on n a (λ _, b)

lemma lemma1 (a b c : ℕ)  : a.case b c = b :=
begin
  admit
end

example (a b c : ℕ) : nat.case a b c = b :=
begin
  extract_goal lemma1,
  exact lemma1 a b c, -- error
end

[Mario Carneiro]

I'm pretty sure this is a bug in the pretty printer. It's never supposed to fail a round-trip like this

[Mario Carneiro]

I think the pretty printer should use the same algorithm as the parser in this case, which would mean that c.case a b means nat.case a b c, using the first variable that has the right type given the unsubstituted type of the constant

[Shing Tak Lam]

Mario Carneiro said:

I'm pretty sure this is a bug in the pretty printer. It's never supposed to fail a round-trip like this

Should I file this to leanprover-community/lean as a bug? (ie. make an issue)?

[Shing Tak Lam]

lean#268