[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:
http://code.google.com/p/agda/issues/detail?id=408
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/
More information about the Agda
mailing list