Вызов функции в Агде

Question

У меня есть этот код, который в основном представляет собой hello world, с функцией добавления, он компилирует и запускает и выводит "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!"

Как мне позвонить _+_ функционировать? Моя цель позвонить _+_ с двумя аргументами вроде _+_(3,4) и получить программу для вывода семи.

Моя интуиция говорит, чтобы заменить линию " main = putStrLn "Hello, world 5!""с чем-то вроде"putStrLn _+_(3,4)'

Я новичок в Agda, и в Интернете не так много примеров рабочего кода. Кто-нибудь может заставить эту функцию работать, приводя практический пример кода?

Спасибо!

Answer 1

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)) ++ "!")