## Stream: new members

### Topic: why does an anonymous assume need extra colon?

#### Fames Yasd (Sep 09 2020 at 09:12):

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 (Sep 09 2020 at 09:13):

How do you use have without a colon?

#### Fames Yasd (Sep 09 2020 at 09:16):

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 (Sep 09 2020 at 09:16):

In term mode you can use have without colon

yes

#### Johan Commelin (Sep 09 2020 at 09:17):

@Fames Yasd Pro tip: #backticks

#### Fames Yasd (Sep 09 2020 at 09:17):

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

#### Fames Yasd (Sep 09 2020 at 09:17):

Johan Commelin thank you

#### Johan Commelin (Sep 09 2020 at 09:19):

assume f x


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

#### Fames Yasd (Sep 09 2020 at 09:22):

so the ambiguity rises because we can assume several statements?

#### Fames Yasd (Sep 09 2020 at 09:22):

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

#### Fames Yasd (Sep 09 2020 at 09:23):

could have made it in a separate keyword like assumptions

#### Fames Yasd (Sep 09 2020 at 09:24):

maybe not, anyway thanks for the info

#### Johan Commelin (Sep 09 2020 at 09:25):

But assume x y z reads more natural, right?

yes

#### Johan Commelin (Sep 09 2020 at 09:25):

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

Last updated: May 18 2021 at 16:25 UTC