<br><div class="gmail_quote">On Fri, Mar 5, 2010 at 11:31 AM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cs.nott.ac.uk">nad@cs.nott.ac.uk</a>></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'm not certain that there aren't any gotchas, but it might be worth looking into.</div>
<div><br></div><div>/ Ulf </div></div>