Stream: Coq users

Topic: TC failure inside Ltac `match`?


view this post on Zulip Ralf Jung (Jun 23 2021 at 07:18):

I am seeing some very strange behavior... in this goal

  h : mem
  _0, _1 : Z
  ============================
  Decision (scalar_eq h _0 _1)

doing destruct (decide (_0 = _1)). works fine, but

    match goal with |- context[scalar_eq _ ?l ?r] => destruct (decide (l = r)) as [ -> | ] end.

fails saying

Error:
Unable to satisfy the following constraints:
In environment:
h : mem
_0, _1 : Z

?Decision : "Decision (_0 = _1)"

(which is utter nonsense, of course we have that instance for Z equality)

view this post on Zulip Ralf Jung (Jun 23 2021 at 07:19):

oh, there might be some coercions here

view this post on Zulip Ralf Jung (Jun 23 2021 at 07:19):

yeah that was it


Last updated: Feb 04 2023 at 21:02 UTC