[Agda] why it can no be parsed ?

[gallais at EnsL]

Hi Leonardo,

The character ')' is reserved :
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.LexicalMatters

Cheers,
--
gallais



On 15 July 2010 00:04, Leonardo Rodriguez
<leonardomatiasrodriguez at gmail.com> wrote:
> Hi,
> this is the problem:
>
> 〈_⟩ : {c : Ctx}{t : Type}  -> Exp c t  -> GExp
> ⟨ NCon x φ ⟩ = GNCon x
> ... the other cases ...
>
> error:
>
> Could not parse the left-hand side ⟨ NCon x φ ⟩
> when scope checking the left-hand side ⟨ NCon x φ ⟩ in the
> definition of 〈_⟩
>
> Thank you in advance
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>