Zulip Chat Archive

Stream: general

Topic: has_one but expected has_zero


view this post on Zulip 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 ℕ

view this post on Zulip 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).

view this post on Zulip Scott Morrison (Feb 09 2019 at 00:39):

Ahh

view this post on Zulip Scott Morrison (Feb 09 2019 at 00:39):

it is to_additives fault.

view this post on Zulip Mario Carneiro (Feb 09 2019 at 00:42):

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

view this post on Zulip Mario Carneiro (Feb 09 2019 at 00:42):

there are lots of examples in group_power of manual to_additive

view this post on Zulip Scott Morrison (Feb 09 2019 at 00:45):

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

view this post on Zulip Kenny Lau (Feb 09 2019 at 00:46):

deja vu

view this post on Zulip Kenny Lau (Feb 09 2019 at 00:46):

this all feels like discussed before

view this post on Zulip Scott Morrison (Feb 09 2019 at 00:50):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Feb 09 2019 at 01:13):

got it, thanks, that works no problem


Last updated: May 15 2021 at 00:39 UTC