Zulip Chat Archive

Stream: lean4

Topic: simp type error

Mario Carneiro (Dec 18 2021 at 02:22):

MWE:

example (a : α) : ¬ some (some a) = some none := by simp

(kernel) declaration type mismatch, 'Option._example' has type
  ∀ {α : Type u_1} (a : α), ¬some a = none
but it is expected to have type
  ∀ {α : Type u_1} (a : α), ¬some (some a) = some none

Leonardo de Moura (Dec 18 2021 at 14:51):

Pushed a fix for this bug.

Last updated: Dec 20 2023 at 11:08 UTC