[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