[Agda] why it can no be parsed ?

[Chris Casinghino]

Hi Leonardo,

Perhaps it isn't apparent in your font, but you have used a different
left angle brackets on the two lines.  The first is U+2329, agda's
\langle, and the second is U+27E8, agda's \<.  They look identical in
my emacs font as well - luckily they look different in gmail.

--Chris

On Wed, Jul 14, 2010 at 6:04 PM, 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
>
>