[Agda] why it can no be parsed ?

Leonardo Rodriguez leonardomatiasrodriguez at gmail.com
Thu Jul 15 00:04:47 CEST 2010


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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100714/88875877/attachment.html


More information about the Agda mailing list