# Zulip Chat Archive

## Stream: new members

### Topic: How does polymorphism work in Lean?

#### YH (Dec 11 2019 at 06:23):

For example, if I want to write

lemma tN (a b : ℕ) (a > 0) : (a + b > b) := sorry lemma tQ (a b : ℚ) (a > 0) : (a + b > b) := sorry lemma tR (a b : ℝ) (a > 0) : (a + b > b) := sorry

how do I convince Lean that the 2nd `+`

is for ℚ and the 3rd `+`

is for `ℝ`

? Lean doesn't seem happy if I just write it like that. (Same question for `>`

.)

#### Johan Commelin (Dec 11 2019 at 06:39):

@YH This solves your error message:

lemma tN (a b : ℕ) (h : a > 0) : (a + b > b) := sorry lemma tQ (a b : ℚ) (h : a > 0) : (a + b > b) := sorry lemma tR (a b : ℝ) (h : a > 0) : (a + b > b) := sorry

#### Johan Commelin (Dec 11 2019 at 06:39):

The problem was with the positivity assumption

#### YH (Dec 11 2019 at 06:40):

Oh, OK. Let me check it out.

#### Johan Commelin (Dec 11 2019 at 06:40):

Try eg:

lemma tQ (a b : ℚ) (a > 0) : true := begin -- cursor here end

#### Johan Commelin (Dec 11 2019 at 06:41):

You'll see that the 2nd `a`

in the statement is introduced as a new variable of type `nat`

#### Johan Commelin (Dec 11 2019 at 06:41):

I don't know why... it looks a bit buggy to me. But explicitly naming the hypothesis solves the issue

#### YH (Dec 11 2019 at 06:42):

Yes it works, thanks.

#### Kevin Buzzard (Dec 11 2019 at 15:04):

Hypotheses before the colon need to be named, right?

I would avoid `y > x`

if you can. Replace it with `x < y`

.

#### Rob Lewis (Dec 11 2019 at 15:07):

I think the acceptance of `(a > 0)`

is a "feature" related to the parsing of `∀ x > 0`

. Not sure how intentional it is.

#### Marc Huisinga (Dec 11 2019 at 15:12):

lemma a (α : Type*) (xs : list α) (x : α) (h : x ∈ xs) : true := sorry lemma b (α : Type*) (xs : list α) (x ∈ xs) : true := sorry lemma c (α : Type*) (xs : list α) : Π x ∈ xs, true := sorry

all yield the same type when using `check`

Last updated: Dec 20 2023 at 11:08 UTC