Hi, <br>this is the problem: <br><br>〈_⟩ : {c : Ctx}{t : Type}  -&gt; Exp c t  -&gt; GExp<br>⟨ NCon x φ ⟩ = GNCon x<br>... the other cases ...<br><br>error:<br><br>Could not parse the left-hand side ⟨ NCon x φ ⟩<br>when scope checking the left-hand side ⟨ NCon x φ ⟩ in the<br>
definition of 〈_⟩<br><br>Thank you in advance<br><br><br>