[Agda] wierd error

[Ulf Norell]

On Thu, Jan 28, 2010 at 4:19 PM, Ruben Henner Zilibowitz <
rzilibowitz at yahoo.com.au> wrote:

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

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

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100128/dce0e24c/attachment.html