[Agda] Absurd catch all pattern

[Ulf Norell]

On Fri, Mar 5, 2010 at 11:31 AM, Nils Anders Danielsson
<nad at cs.nott.ac.uk>wrote:

> On 2010-03-04 21:14, Andreas Abel wrote:
>
>> Is it thinkable to get this accepted?
>>
>
> Perhaps it would even be possible to get the following code accepted:
>
>  _≟_ : (x y : Bool) → Dec (x ≡ y)
>  true  ≟ true  = yes refl
>  false ≟ false = yes refl
>  _     ≟ _     = no (λ ())
>
> Ulf and I have discussed this in the past. There are some issues: ...
>

Most of these issues disappear if we only allow expansion for absurd
clauses. I'm not certain that there aren't any gotchas, but it might be
worth looking into.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100305/c4c8754f/attachment.html