agda

.gitignore

*agdai
MAlonzo

Bool.agda

module Bool where

data Bool : Set where
  True : Bool
  False : Bool

_&&_ : Bool -> Bool -> Bool
True && b = b
False && b = False

_||_ : Bool -> Bool -> Bool
True || b = True
False || b = b

~_ : Bool -> Bool
~ True = False
~ False = True

_xor_ : Bool -> Bool -> Bool
True xor b = ~ b
False xor b = b

if_then_else_ : ∀ {A : Set} -> Bool -> A -> A -> A
if True then l else r = l
if False then l else r = r

_nor_ : Bool -> Bool -> Bool
a nor b = ~ (a || b)

_nand_ : Bool -> Bool -> Bool
a nand b = ~ (a && b)

BoolTheorem.agda

module BoolTheorem where

open import Bool
open import Eq

doubleNeg : ∀ (b : Bool) -> (~ ~ b) ≡ b
doubleNeg True = refl
doubleNeg False = refl

andIdem : ∀ (b : Bool) -> (b && b) ≡ b
andIdem True = refl
andIdem False = refl

orIdem : ∀ (b : Bool) -> (b || b) ≡ b
orIdem True = refl
orIdem False = refl

Day.agda

module Day where

data Bool : Set where
  True : Bool
  False : Bool

data Day : Set where
  Monday : Day
  Tuesday : Day
  Wednesday : Day
  Thursday : Day
  Friday : Day
  Saturday : Day
  Sunday : Day

nextDay : Day -> Day
nextDay Monday = Tuesday
nextDay Tuesday = Wednesday
nextDay Wednesday = Thursday
nextDay Thursday = Friday
nextDay Friday = Saturday
nextDay Saturday = Sunday
nextDay Sunday = Monday

data Suit : Set where
  Spade : Suit
  Diamond : Suit
  Heart : Suit
  Clubs : Suit

is-red : Suit -> Bool
is-red Spade = False
is-red Diamond = True
is-red Heart = True
is-red Clubs = False

Eq.agda

module Eq where

data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
  refl : x ≡ x