forall/pi bug

Stream: general

[Kenny Lau]

#mwe:

constant foo : ∀ {α : Type}, (∀ x : α, true → ∀ y : α, x = x)
#check foo

Error: the forall ∀ is converted to a pi Π in the suggestions.

Minimality: the following changes makes the bug disappear:

• making α into any concrete type (e.g. ℕ)
• removing the dependence of x = x on x (e.g. by changing it to true)
• making the type of y a concrete type
• removing true →
• removing ∀ y : α,

[Bryan Gin-ge Chen]

Changing the curly braces around α to parentheses also makes the bug disappear.

[Bryan Gin-ge Chen]

I think this line of shell/completion.cpp is where the completions are returned (if you have ideas about improving the suggestions, this file is also the place to start digging), and that calls "serialize_decl" to format the name and type. I can't look further at the moment, but maybe you can see what the issue is.

[Scott Viteri]

Is this an instance of the same bug, or something different?

universe u
variable (α : Type u)
inductive pairwise (R : α → α → Prop) : list α → Prop
| nil : pairwise (@list.nil α)
| cons : ∀ {a : α} {l : list α},
    (∀ a':α, mem a' l → R a a') → pairwise l → pairwise (list.cons a l)

28:14: type mismatch at application
  mem a'
term
  a'
has type
  α : Type u
but is expected to have type
  Type ? : Type (?+1)

[Mario Carneiro]

what is mem?

[Scott Viteri]

Where list and mem are explicitly defined in the current namespace

[Scott Viteri]

def mem : α → list α → Prop
| a  list.nil       := false
| a (list.cons b l) := a = b ∨ mem a l

[Mario Carneiro]

#mwe

[Kevin Buzzard]

(deleted)

[Scott Viteri]

alright, my bad will create mwe

[Mario Carneiro]

What is the type of mem

[Mario Carneiro]

#print mem -- ???

[Kevin Buzzard]

there is something wrong with your mem a' and it looks like you've just fed it a bad term but it's hard to tell if you don't post working code. As Mario said, if you look at the type of mem it will probably tell you what you did wrong.

[Scott Viteri]

α → list α → Prop

[Mario Carneiro]

that's an open term, I don't believe you

[Kevin Buzzard]

Is that the actual output of #check @mem?

[Mario Carneiro]

I notice also that in your post you wrote variable (α : Type u)

[Scott Viteri]

yes

[Kevin Buzzard]

My guess is that mem wants to be fed an explicit type i.e. alpha, and if you look at the actual type you'll see this.

[Mario Carneiro]

if you defined mem after that then it will pick up this explicit alpha

[Scott Viteri]

It takes a second to write the output of check since I can't copy paste minibuffer

[Scott Viteri]

I'm on it though

[Mario Carneiro]

there is a copy button

[Mario Carneiro]

oh you mean emacs

[Scott Viteri]

yes

[Mario Carneiro]

you should be able to copy from the problems panel or sidekick or whatever it's called

[Scott Viteri]

#check @mem
--mem : Π (α : Type u_1), α → list α → Prop

[Mario Carneiro]

boom

[Mario Carneiro]

parentheses means explicit alpha

[Jannis Limperg]

On Emacs, you can open the buffer Lean Goal or Lean Errors and copy out of that.

[Mario Carneiro]

so you have to write mem _ a' l

[Scott Viteri]

Oh I figured out how to copy from minibuffer

[Mario Carneiro]

or else use variable {α : Type u} at the top of the file

[Kevin Buzzard]

and probably the same for R

[Mario Carneiro]

Not in pairwise, I think

[Mario Carneiro]

you want pairwise R l not pairwise _ l

[Scott Viteri]

Jannis Limperg said:

On Emacs, you can open the buffer Lean Goal or Lean Errors and copy out of that.

oh yeah that works too, I was just going to messages

[Scott Viteri]

Mario Carneiro said:

or else use variable {α : Type u} at the top of the file

Why?

[Scott Viteri]

oh I see, sorry reading different threads

[Kyle Miller]

Scott Viteri said:

Jannis Limperg said:

On Emacs, you can open the buffer Lean Goal or Lean Errors and copy out of that.

oh yeah that works too, I was just going to messages

The Lean Errors buffer (C-c C-n) is also where you can get #print and #lint messages for copy/paste.

[Scott Viteri]

Ok fixed thx for the super fast responses

[Scott Viteri]

I didn't realize that the errors buffer also takes output from commands

[Kyle Miller]

(Also, while you can't copy paste them, you can use C-c C-b to get inline command output.)

[Scott Viteri]

Yeah that's a nice feature