Zulip Chat Archive

Stream: general

Topic: pretty printer uses projection notation only for first arg


view this post on Zulip 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
-/

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 24 2020 at 10:24):

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

view this post on Zulip Kenny Lau (May 24 2020 at 10:24):

is this the intended behaviour?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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 : ℕ

view this post on Zulip Mario Carneiro (May 24 2020 at 11:26):

Here's another fun one:

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

view this post on Zulip 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
  admit
end

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)?

view this post on Zulip Shing Tak Lam (May 24 2020 at 13:17):

lean#268


Last updated: May 15 2021 at 00:39 UTC