## Stream: general

### Topic: has_one but expected has_zero

#### Scott Morrison (Feb 09 2019 at 00:37):

Woah... Lean confused by the difference between zero and one?

error: type mismatch at application
0
term
nat.has_one
has type
has_one ℕ
but is expected to have type
has_zero ℕ


#### Scott Morrison (Feb 09 2019 at 00:38):

This is generated in the (apparently innocuous?)

lemma Ico_prod_split_first (n m : ℕ) (h₁ : n < m) (f : ℕ → β) :
(Ico n m).prod f = f n * (Ico (n+1) m).prod f := ...


The error appears on the 1 in Ico (n+1).

Ahh

#### Scott Morrison (Feb 09 2019 at 00:39):

it is to_additives fault.

#### Mario Carneiro (Feb 09 2019 at 00:42):

that happens, especially when you mix your type beta with nat

#### Mario Carneiro (Feb 09 2019 at 00:42):

there are lots of examples in group_power of manual to_additive

#### Scott Morrison (Feb 09 2019 at 00:45):

so it's okay to just reprove it, copying and pasting the proof?

deja vu

#### Kenny Lau (Feb 09 2019 at 00:46):

this all feels like discussed before

#### Scott Morrison (Feb 09 2019 at 00:50):

Sorry, @Kenny Lau, but of course I can't read everything here.

#### Mario Carneiro (Feb 09 2019 at 00:57):

better than copy and paste the proof, you will notice that most of the group_power theorems are proven by applying the original theorem via multiplicative

#### Scott Morrison (Feb 09 2019 at 01:13):

got it, thanks, that works no problem

Last updated: May 15 2021 at 00:39 UTC