[Agda] Question about inequality and absurd patterns

[Jesper Cockx]

Hi Bill,

This is an unfortunate bug in the latest release of Agda, see
https://github.com/agda/agda/issues/4882. It's already been fixed on the
development version, so the fix should come once 2.6.2 is released.

-- Jesper

On Fri, Oct 2, 2020 at 12:33 AM <mechvel at scico.botik.ru> wrote:

> On 2020-10-01 23:19, William Harrison wrote:
> > Hi-
> >
> >      I have a question about proving inequalities (≢) in Agda. It's
> > probably such a stupid question that I should be embarrassed for
> > asking it, but, fortunately, I lost my capacity to feel embarrassment
> > years ago.
> >
> > In the following Agda code, the "good" definition works, but the "bad"
> > one does not and yields the commented complaint. I assume that (≢)
> > insists on literal term equality and that is the source of the
> > different responses from Agda. Is there any way of evaluating under
> > the (≢)? I'm formulating a typed language using strings for
> > variables, and so this sort of inequality calculation is involving in
> > variable dereference. I've attached a minimal example. Thanks in
> > advance.
> >
> >> good : "x" ≢ "y"
> >>
> >> good ()
> >>
> >> bad : "x" ≢ Data.Vec.head ("y" ∷ "y" ∷ [])
> >>
> >> bad ()
> >>
> >> {-
> >>
> >> Failed to solve the following constraints:
> >>
> >> Is empty: "x" ≡ head ("y" ∷ "y" ∷ [])
> >>
> >> [ at <...snip...>/MinimalExample.agda:11,5-7 ]
> >>
> >> -}
>
> And
>      bad = good
>
> is type-checked (in Agda 2.6.1).
> I do not guess what is the matter.
>
> --
> SM
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201002/da3c73d2/attachment.html>