Zulip Chat Archive

Stream: new members

Topic: motive is not type correct with coe


view this post on Zulip Eric Wieser (Jun 29 2020 at 12:32):

My state is:

q : (x + y) = x + y
 fₛ r_1 * (x + y), _⟩ = fₛ r_1 * x, _⟩ + fₛ r_1 * y, _⟩

and the obvious strategy would be rw q. However, this fails with

rewrite tactic failed, motive is not type correct
  λ (_a : G),
    fₛ r_1 * (x + y), _⟩ = fₛ r_1 * x, _⟩ + fₛ r_1 * y, _⟩ =
      (fₛ r_1 * (x + y), _⟩ = fₛ r_1 * x, _⟩ + fₛ r_1 * y, _⟩)

Two questions then:

  • How should I read this error message?
  • Why won't q substitute?

view this post on Zulip Eric Wieser (Jun 29 2020 at 12:33):

Nevermind, I can't read. The error message is confusing though.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 13:51):

simp only [q] might make progress


Last updated: May 14 2021 at 05:20 UTC