Search code examples
agda

Parse Errors in Agda in terms of definition

I am new to Agda and trying to understand the syntax of Agda. I am trying to define the power operator in Agda:^. Here is my code:

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)
data N : Set where
zero : N
suc : N -> N
{-# BUILTIN NATURAL N #-}

_+_ : N → N → N
  zero + n = n
 (suc m) + n = suc (m + n)

_*_ : N -> N -> N
  zero * N = zero
  (suc m) * n = n + (m * n)

 one = suc zero 
 _^_ : N -> N -> N 
   m ^ zero = one
   m ^ (1 + n)  =  m * (m ^ n)

And I get the error message : /home/mirage/Agda/power.agda:19,13: Parse error = one m ^ (1 + n) = m * (m...

Can anyone help me with it?

Thanks in advance!!!!

Solution

  • You're indenting the clauses defining a function under its declaration but Agda expect them to be at the same level. So:

    _+_ : N → N → N
zero + n = n
(suc m) + n = suc (m + n)

    (and the same for the other functions).