<br><br><div class="gmail_quote">On Thu, Dec 3, 2009 at 4:20 AM, Vag Vagoff <span dir="ltr">&lt;<a href="mailto:vag.vagoff@gmail.com">vag.vagoff@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">

How to make use of big brackets and parentheses? Parser complains at [_]: {A : &gt;&gt;&gt; here &lt;&lt;&lt; Set} → A → A<br>
<br>
 -- [ ] --<br>
[_]: {A : Set} → A → A<br>
[a] = a<br>
<br></blockquote><div><br>White spaces have to be inserted<br><br>[ a ]  = a<br><br><br> </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">


-- ( ) --<br>
(_): {A : Set} → A → A<br>
( a )= a<br></blockquote><div><br><br>Parentheses cannot be a character of a name part<br><em></em><a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.LexicalMatters">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.LexicalMatters</a><br clear="all">

</div></div><br>-- <br>Andrés<br>