<div dir="ltr"><div>Hi Bill,</div><div><br></div><div>This is an unfortunate bug in the latest release of Agda, see <a href="https://github.com/agda/agda/issues/4882">https://github.com/agda/agda/issues/4882</a>. It's already been fixed on the development version, so the fix should come once 2.6.2 is released.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Oct 2, 2020 at 12:33 AM <<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 2020-10-01 23:19, William Harrison wrote:<br>
> Hi-<br>
> <br>
>      I have a question about proving inequalities (≢) in Agda. It's<br>
> probably such a stupid question that I should be embarrassed for<br>
> asking it, but, fortunately, I lost my capacity to feel embarrassment<br>
> years ago.<br>
> <br>
> In the following Agda code, the "good" definition works, but the "bad"<br>
> one does not and yields the commented complaint. I assume that (≢)<br>
> insists on literal term equality and that is the source of the<br>
> different responses from Agda. Is there any way of evaluating under<br>
> the (≢)? I'm formulating a typed language using strings for<br>
> variables, and so this sort of inequality calculation is involving in<br>
> variable dereference. I've attached a minimal example. Thanks in<br>
> advance.<br>
> <br>
>> good : "x" ≢ "y"<br>
>> <br>
>> good ()<br>
>> <br>
>> bad : "x" ≢ Data.Vec.head ("y" ∷ "y" ∷ [])<br>
>> <br>
>> bad ()<br>
>> <br>
>> {-<br>
>> <br>
>> Failed to solve the following constraints:<br>
>> <br>
>> Is empty: "x" ≡ head ("y" ∷ "y" ∷ [])<br>
>> <br>
>> [ at <...snip...>/MinimalExample.agda:11,5-7 ]<br>
>> <br>
>> -}<br>
<br>
And<br>
     bad = good<br>
<br>
is type-checked (in Agda 2.6.1).<br>
I do not guess what is the matter.<br>
<br>
--<br>
SM<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>