Zulip Chat Archive

Stream: general

Topic: forall/pi bug


view this post on Zulip Kenny Lau (Jul 26 2020 at 17:53):

#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 : α,

view this post on Zulip Bryan Gin-ge Chen (Jul 26 2020 at 18:01):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 26 2020 at 18:08):

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.

view this post on Zulip Scott Viteri (Aug 16 2020 at 17:48):

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)

view this post on Zulip Mario Carneiro (Aug 16 2020 at 17:49):

what is mem?

view this post on Zulip Scott Viteri (Aug 16 2020 at 17:49):

Where list and mem are explicitly defined in the current namespace

view this post on Zulip Scott Viteri (Aug 16 2020 at 17:49):

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

view this post on Zulip Mario Carneiro (Aug 16 2020 at 17:49):

#mwe

view this post on Zulip Kevin Buzzard (Aug 16 2020 at 17:49):

(deleted)

view this post on Zulip Scott Viteri (Aug 16 2020 at 17:50):

alright, my bad will create mwe

view this post on Zulip Mario Carneiro (Aug 16 2020 at 17:50):

What is the type of mem

view this post on Zulip Mario Carneiro (Aug 16 2020 at 17:50):

#print mem -- ???

view this post on Zulip Kevin Buzzard (Aug 16 2020 at 17:50):

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.

view this post on Zulip Scott Viteri (Aug 16 2020 at 17:50):

α → list α → Prop

view this post on Zulip Mario Carneiro (Aug 16 2020 at 17:51):

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

view this post on Zulip Kevin Buzzard (Aug 16 2020 at 17:51):

Is that the actual output of #check @mem?

view this post on Zulip Mario Carneiro (Aug 16 2020 at 17:52):

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

view this post on Zulip Scott Viteri (Aug 16 2020 at 17:52):

yes

view this post on Zulip Kevin Buzzard (Aug 16 2020 at 17:52):

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.

view this post on Zulip Mario Carneiro (Aug 16 2020 at 17:52):

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

view this post on Zulip Scott Viteri (Aug 16 2020 at 17:52):

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

view this post on Zulip Scott Viteri (Aug 16 2020 at 17:52):

I'm on it though

view this post on Zulip Mario Carneiro (Aug 16 2020 at 17:52):

there is a copy button

view this post on Zulip Mario Carneiro (Aug 16 2020 at 17:53):

oh you mean emacs

view this post on Zulip Scott Viteri (Aug 16 2020 at 17:53):

yes

view this post on Zulip Mario Carneiro (Aug 16 2020 at 17:53):

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

view this post on Zulip Scott Viteri (Aug 16 2020 at 17:53):

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

view this post on Zulip Mario Carneiro (Aug 16 2020 at 17:53):

boom

view this post on Zulip Mario Carneiro (Aug 16 2020 at 17:54):

parentheses means explicit alpha

view this post on Zulip Jannis Limperg (Aug 16 2020 at 17:54):

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

view this post on Zulip Mario Carneiro (Aug 16 2020 at 17:54):

so you have to write mem _ a' l

view this post on Zulip Scott Viteri (Aug 16 2020 at 17:54):

Oh I figured out how to copy from minibuffer

view this post on Zulip Mario Carneiro (Aug 16 2020 at 17:54):

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

view this post on Zulip Kevin Buzzard (Aug 16 2020 at 17:54):

and probably the same for R

view this post on Zulip Mario Carneiro (Aug 16 2020 at 17:54):

Not in pairwise, I think

view this post on Zulip Mario Carneiro (Aug 16 2020 at 17:55):

you want pairwise R l not pairwise _ l

view this post on Zulip Scott Viteri (Aug 16 2020 at 17:55):

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

view this post on Zulip Scott Viteri (Aug 16 2020 at 17:56):

Mario Carneiro said:

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

Why?

view this post on Zulip Scott Viteri (Aug 16 2020 at 17:56):

oh I see, sorry reading different threads

view this post on Zulip Kyle Miller (Aug 16 2020 at 17:57):

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.

view this post on Zulip Scott Viteri (Aug 16 2020 at 17:57):

Ok fixed thx for the super fast responses

view this post on Zulip Scott Viteri (Aug 16 2020 at 17:59):

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

view this post on Zulip Kyle Miller (Aug 16 2020 at 17:59):

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

view this post on Zulip Scott Viteri (Aug 16 2020 at 18:00):

Yeah that's a nice feature


Last updated: May 11 2021 at 12:15 UTC