[Agda] wierd error

[Ruben Henner Zilibowitz]

Hi,

I am getting what seems like a wierd error that I can't debug. If someone could take a look and help fix this it would be quite instructive. Thanks. I'm using agda 2.2.6 with lib-0.2.

WierdError.agda:11,43-12,10
Could not parse the application begin + ∣ + m
when scope checking begin + ∣ + m

----------

module WierdError where

open import Data.Integer
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

∣∣-dist-≡ : ∀ {x y} → x ≡ y → + ∣ x ∣ ≡ + ∣ y ∣
∣∣-dist-≡ { -[1+ m ] } { -[1+ n ] } x≡y = {!!}
∣∣-dist-≡ { -[1+ m ] } { +    n }   x≡y = {!!}
∣∣-dist-≡ { +    m }   { -[1+ n ] } x≡y = {!!}
∣∣-dist-≡ { +    m }   { +    n }   x≡y = begin
  + ∣ + m | ≡⟨ refl ⟩
  + m ≡⟨ x≡y ⟩
  + n ≡⟨ refl ⟩
  + ∣ + n ∣ ∎

------------

Regards,

Ruben