## Stream: general

### Topic: pretty printer uses projection notation only for first arg

#### Kenny Lau (May 24 2020 at 10:24):

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 (May 24 2020 at 10:24):

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 (May 24 2020 at 10:24):

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

#### Kenny Lau (May 24 2020 at 10:24):

is this the intended behaviour?

#### Kenny Lau (May 24 2020 at 10:26):

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 (May 24 2020 at 11:08):

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

#### Mario Carneiro (May 24 2020 at 11:23):

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 (May 24 2020 at 11:26):

Here's another fun one:

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


#### Shing Tak Lam (May 24 2020 at 11:53):

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
end

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


#### Mario Carneiro (May 24 2020 at 11:56):

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 (May 24 2020 at 11:58):

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 (May 24 2020 at 12:35):

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 (May 24 2020 at 13:17):

lean#268

Last updated: May 15 2021 at 00:39 UTC