<br><div class="gmail_quote">On Wed, Oct 13, 2010 at 11:01 AM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
2. Why is<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
isTrue : Bool -> Set<br>
isTrue true = True<br>
isTrue false = False<br>
</blockquote>
valid but not the reverse, i.e.<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
isBool : Set -> Bool<br>
isBool True = true<br>
isBool False = false<br>
</blockquote>
isn't?<br>
</blockquote>
<br>
This is a real design problem of Agda: What parts of a pattern are variables bound by the pattern is too context sensitive.<br>
<br>
It needs to be clear from apparition alone which are the constructors and which are the variables. Haskell solves this by putting constructors into a different class of identifiers. We need a some way to distinguish variables from constructors in patterns, and there are >=3 choices:<br>
</blockquote><div><br></div><div>Variables and constructors are distinguished by colour. I can't remember what the default colours are but if you think the difference is too subtle you can always change your preferences to make it more obvious.</div>
<div><br></div><div>/ Ulf </div></div>