[Agda] Big brackets: parse error

[Andrés Sicard-Ramírez]

On Thu, Dec 3, 2009 at 4:20 AM, Vag Vagoff <vag.vagoff at gmail.com> wrote:

> How to make use of big brackets and parentheses? Parser complains at ［_］:
> {A : >>> here <<< Set} → A → A
>
>  -- [ ] --
> ［_］: {A : Set} → A → A
> ［a］ = a
>
>
White spaces have to be inserted

[ a ]  = a




> -- ( ) --
> （_）: {A : Set} → A → A
> （ a ）= a
>


Parentheses cannot be a character of a name part
**
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.LexicalMatters

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091203/6b22d562/attachment.html