[Agda] wierd error

[Ruben Henner Zilibowitz]

Ok. Thanks. Now how do I write this function?

∣∣-pres-≡ : {x y : ℤ} → x ≡ y → ∣ x ∣ ≡ ∣ y ∣

Ruben

On 28/01/2010, at 11:23 PM, Ulf Norell wrote:

> 
> On Thu, Jan 28, 2010 at 12:36 PM, Ruben Henner Zilibowitz <rzilibowitz at yahoo.com.au> wrote:
> Hi,
> 
> If I do that I get a parse error:
> 
> WierdError.agda:12,15:
> Parse error )<ERROR> ≡⟨ refl ⟩ ( + m ) ≡⟨ x≡y ⟩ ....
> 
> Ah, the problem is that you've used the wrong kind of bar. The ascii bar is reserved for the with construct, the abs function uses U+2223 which you get by typing \| or \mid in the Agda input method.
> 
> / Ulf

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100129/2add083b/attachment.html