# [Agda] Absurd pattern; convincing Agda

Andreas Abel andreas.abel at ifi.lmu.de
Tue Jun 12 16:54:56 CEST 2012

```Hi Paul,

this is how to convince Agda.  Just split one level deeper:

withoutEQ (def f (x ∷ [])) () | no ¬p
withoutEQ (def f (x ∷ x₁ ∷ xs)) () | no ¬p

Now the unsolved meta is gone.

The problem was that the equations given for a match do not always hold
literally.  In you case, this equation does not reduce:

outerIsEq (def f (x ∷ xs)) | no ¬p = false

This is because internally, Agda decided it wants to split on xs before
reducing.  I'd consider this unwanted behavior on the side of Agda. See:

In a simple case, consider the equations

and : Bool -> Bool -> Bool
and false x = false
and y false = false
and _ _     = true

One of

and false x
and y false

will not reduce to false, since Agda converts this definition into a
case tree, so it will either match on the first (likely) or the second
argument.  So you will likely get the equations

and false x    = false
and true false = false
and true true  = true

and the type

and y false == false

will not be empty.

Why in your specific case you do not get the equations you specified, I
cannot tell.

Hope that helps.

Cheers,
Andreas

On 12.06.2012 14:36, Paul van der Walt wrote:
> Dear all,
>
> I asked this question on IRC, but it was rather quiet there, so
> maybe someone here could help me out.
>
> I am using the Reflection API, and I'd like to manipulate a
> value of type Term which is returned by quoteTerm. I have a
> function which only works for Terms of the form (something ==
> true), and this function should return the LHS if the Term has
> this form. To make this function total, I also have a
> predicate (validity of input checker) which only returns true
> for the cases I want to take care of. See the functions here:
> http://hpaste.org/69846 (excuse the formatting)
>
> The problem is, one of the absurd patterns is accepted by Agda,
> but remains yellow. This causes problems when trying to use the
> module elsewhere. I can clearly see that this case can never be
> reached (order of patterns matters here), but Agda doesn't
> believe me.
>
> Does anyone know how I can solve this? Maybe my approach is
> really ugly?
>
> Thanks in advance, I hope my question is clear enough.
>
> Cheers,
> Paul van der Walt
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
```