## 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: May 15 2021 at 22:14 UTC