Skip to content

Instantly share code, notes, and snippets.

@agam agam/dummy.agda
Created Dec 4, 2018

Embed
What would you like to do?
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 + 35
_ =
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
You can’t perform that action at this time.