has_one but expected has_zero

Stream: general

[Scott Morrison]

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]

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).

[Scott Morrison]

Ahh

[Scott Morrison]

it is to_additives fault.

[Mario Carneiro]

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

[Mario Carneiro]

there are lots of examples in group_power of manual to_additive

[Scott Morrison]

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

[Kenny Lau]

deja vu

[Kenny Lau]

this all feels like discussed before

[Scott Morrison]

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

[Mario Carneiro]

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]

got it, thanks, that works no problem