First steps with 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 | |
∎ | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment