Zulip Chat Archive

Stream: new members

Topic: getting more information on an error


view this post on Zulip Michael Beeson (Oct 06 2020 at 21:13):

I know there is a way to get a more elaborate error message but I have forgotten what it is. I have the following error that is
mysterious to me. It complains about the type of "a" but I don't see anything wrong. It is complaining at
this input line:

     have h50:  (p q:M), p  USC a  q  USC a  ¬ p = q  (p  q = Λ ) :=

and here is the error:

M: Type
_inst_1: Model M
mn: M
h1: m  𝔽
h2: n  𝔽
h4copy:  (u : M), u  exp M n
b: M
h5: USC b  n
h6:  (u : M), u  n
h7: m  n   (b : M), b  n  ( (a : M), a  m  a  b  b = (a  b - a))
h3: USC b  n  ( (a : M), a  m  a  USC b  USC b = (a  USC b - a))
x: M
h21: x  USC b
h22: USC b = (x  USC b - x)
a: M := union x
h9: a = union x
line789: x = USC a
h20: USC a  m
h23: ( (a : M), USC a  m)   (b : M), b  exp M m
h24:  (a : M), USC a  m
bFinite: b  FINITE M
xFinite: USC a  FINITE M
h40:  (u : M), u  USC a  u  FINITE M
 a  FINITE M
All Messages (1)
inf7.lean:1163:8
type mismatch at application
  USC a
term
  a
has type
  p  USC a : Prop
but is expected to have type
  M : Type

view this post on Zulip Kenny Lau (Oct 06 2020 at 21:15):

aha, this is the a bug

view this post on Zulip Kenny Lau (Oct 06 2020 at 21:15):

pick literally any other variable name

view this post on Zulip Reid Barton (Oct 06 2020 at 21:15):

https://github.com/leanprover-community/lean/issues/437

view this post on Zulip Kenny Lau (Oct 06 2020 at 21:15):

The famous a bug doesn't need a description, we have all met it.

view this post on Zulip Johan Commelin (Oct 06 2020 at 21:16):

we hope that this will be fixed in lean 3.5.37...

view this post on Zulip Reid Barton (Oct 06 2020 at 21:17):

Kenny Lau said:

pick literally any other variable name

It's probably also a good idea to avoid _x just in case

view this post on Zulip Mario Carneiro (Oct 06 2020 at 23:09):

@Reid Barton What happened to your PR to turn this into the _x bug?

view this post on Zulip Reid Barton (Oct 07 2020 at 20:11):

Unfortunately it triggered a separate issue lean#447, and then it wasn't clear to me how to proceed

view this post on Zulip Kevin Buzzard (Oct 07 2020 at 21:34):

Call it x_ instead?


Last updated: May 18 2021 at 15:14 UTC