functionfunctional-programmingagdaagda-mode

Calling a function in Agda

I have this code which is basically a hello world, with an addition function, it compiles and runs and outputs 'Hello, world 5!':

open import Common.IO

data  ℕ  : Set  where
 zero  : ℕ
 suc   : ℕ → ℕ

-- how to call a function in agda i.e. '_+_(5, 4)' to get '9' 

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


main = putStrLn "Hello, world 5!"

How do I call my _+_ function? My goal is to call _+_ with two arguments like _+_(3,4) and get the program to output seven.

My intuition says to replace the line ' main = putStrLn "Hello, world 5!"' with something like 'putStrLn _+_(3,4)'

I'm new to Agda, and there aren't many examples online of working code. Can anybody get this function working by giving a practical code example?

Thanks!

Solution 
  • open import Common.IO
open import Data.Nat using (ℕ; zero; suc)
open import Data.Integer using (ℤ; +_; show)
open import Data.String using (_++_)

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

main = putStrLn ("Hello, world " ++ show (+ (3 + 4)) ++ "!")