<br><div class="gmail_quote">On Fri, Mar 5, 2010 at 11:31 AM, Nils Anders Danielsson <span dir="ltr">&lt;<a href="mailto:nad@cs.nott.ac.uk">nad@cs.nott.ac.uk</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im">On 2010-03-04 21:14, Andreas Abel wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Is it thinkable to get this accepted?<br>
</blockquote>
<br></div>
Perhaps it would even be possible to get the following code accepted:<br>
<br>
 _≟_ : (x y : Bool) → Dec (x ≡ y)<br>
 true  ≟ true  = yes refl<br>
 false ≟ false = yes refl<br>
 _     ≟ _     = no (λ ())<br>
<br>
Ulf and I have discussed this in the past. There are some issues: ...<br></blockquote><div><br></div><div>Most of these issues disappear if we only allow expansion for absurd clauses. I&#39;m not certain that there aren&#39;t any gotchas, but it might be worth looking into.</div>
<div><br></div><div>/ Ulf </div></div>