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

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