Zulip Chat Archive

Stream: new members

Topic: Problem with function application


view this post on Zulip Emiel Lanckriet (Jul 25 2020 at 08:48):

I'm going through Mathematics in Lean and I came across an exercise where the environment is

h :  {f :   }, monotone f   {a b : }, f a  f b  a  b,
f :    := λ (x : ), 0,
monof : monotone f,
h' : f 1  f 0
 false

and I want to make a term of the form 1 \leq 0 as follows
have h1 : 1 ≤ 0 := h monof h'.
However, I get the following error:

invalid type ascription, term has type
  ?m_1  ?m_2
but is expected to have type
  1  0

I don't really understand, why I don't get 1 ≤ 0.

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 08:51):

I doubt your 1 is the 1 you want. If you don't say (1 : \R) then it defaults to nat. The error means "I'm looking for two real numbers but all I see is naturals"

view this post on Zulip Emiel Lanckriet (Jul 25 2020 at 08:54):

Thanks, indeed, declaring that I want 1 and 0 to be reals does the trick. Is there anything in the error message that hints that this was the problem?

view this post on Zulip Scott Morrison (Jul 25 2020 at 09:03):

You could probably turn on set_option pp.all true (or some intermediate pretty printer setings, e.g. pp.notation false + pp.implicits true.

view this post on Zulip Scott Morrison (Jul 25 2020 at 09:03):

That would show you what type the le was in.

view this post on Zulip Emiel Lanckriet (Jul 25 2020 at 09:09):

Thanks, it makes the errors to complicated to turn on all the time, but it could help when digging deeper.

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 11:52):

I just know that when the user types 1 it means the natural 1 unless specified otherwise. It's an issue which comes up all the time on this chat

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 11:52):

There's even an issue about it on the natural number game. To fix it you need to hack core lean

view this post on Zulip Reid Barton (Jul 25 2020 at 12:18):

Usually Lean tries to expand whatever part of the expressions don't agree in an error like this--if the two expressions still appear to agree (e.g. here it looks like we could set ?m_1 = 1 and ?m_2 = 0) then usually the reason is that the types are wrong or there is a type class or universe issue.

view this post on Zulip Reid Barton (Jul 25 2020 at 12:19):

I wonder whether it would be sensible for have h : T := e to use e to elaborate T, like def does


Last updated: May 17 2021 at 22:15 UTC