First steps with Agda

dummy.agda

module Dummy where

-- Initial definition

data N : Set where
  zero : N
  suc  : N -> N


-- Allow us to use shorthand

{-# BUILTIN NATURAL N #-}

-- Some equality helpers

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

-- Some operations

-- Addition!

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


-- An example of an addition proof:

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩
    suc ((suc zero) + (suc (suc (suc zero))))
  ≡⟨⟩
    suc (suc (zero + (suc (suc (suc zero)))))
  ≡⟨⟩
    suc (suc (suc (suc (suc zero))))
  ≡⟨⟩
    5
  ∎