## Stream: new members

### Topic: Problem with function application

#### 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.

#### 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"

#### 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?

#### 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.

#### Scott Morrison (Jul 25 2020 at 09:03):

That would show you what type the le was in.

#### 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.

#### 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

#### 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

#### 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.

#### 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