Ralf Jung (Jun 23 2021 at 07:18): 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)
Ralf Jung (Jun 23 2021 at 07:19):oh, there might be some coercions here
Ralf Jung (Jun 23 2021 at 07:19):yeah that was it
Last updated: Oct 13 2024 at 01:02 UTC