why does an anonymous assume need extra colon?

Stream: new members

[Fames Yasd]

There is an explanation in theorems proving in lean:
"In contrast to the usage with have, an anonymous assume needs an extra colon. The reason is that Lean allows us to write assume h to introduce a hypothesis without specifying it, and without the colon it would be ambiguous as to whether the h here is meant as the label or the assumption."
but I didn't get it. I feel like anonymous assume should not have an extra colon because it seems to be the same as have and the last one does not have an extra colon when used anonymously.

[Ruben Van de Velde]

How do you use have without a colon?

[Fames Yasd]

variable f : ℕ → ℕ
variable h : ∀ x : ℕ, f x ≤ f (x + 1)

example : f 0 ≥ f 1 → f 1 ≥ f 2 → f 0 = f 2 :=
assume : f 0 ≥ f 1,
assume t₀ : f 1 ≥ f 2,
have  t₁ : f 0 ≥ f 2, from le_trans ‹f 2 ≤ f 1› ‹f 1 ≤ f 0›,
have f 0 ≤ f 2, from le_trans (h 0) (h 1),
show f 0 = f 2, from le_antisymm this ‹f 0 ≥ f 2›

[Johan Commelin]

In term mode you can use have without colon

[Fames Yasd]

yes

[Johan Commelin]

@Fames Yasd Pro tip: #backticks

[Fames Yasd]

but for some reason I can't use assume without colon

[Fames Yasd]

Johan Commelin thank you

[Johan Commelin]

assume f x

What would this mean?
Are you assuming this : f x or is it assume (f : _) (x : _)?

[Fames Yasd]

so the ambiguity rises because we can assume several statements?

[Fames Yasd]

I did not know that we can assume several statements in a row

[Fames Yasd]

could have made it in a separate keyword like assumptions

[Fames Yasd]

maybe not, anyway thanks for the info

[Johan Commelin]

But assume x y z reads more natural, right?

[Fames Yasd]

yes

[Johan Commelin]

So, personally, I think the extra colon is the better tradeoff