playing around with basic booleans and natural numbers

ci.sh

@@ -0,0 +1,21 @@
+#!/usr/bin/env bash
+
+ide:setup() {
+    brew:install:brew:itself
+    brew tap caskroom/cask
+    brew cask install minikube
+    brew install idris
+
+    minikube start
+    eval $(minikube docker-env)
+
+    docker run -d -v /tmp/.X11-unix/:/tmp/.X11-unix/ \
+                -v /dev/shm:/dev/shm \
+                -v ${HOME}/.atom:/home/atom/.atom \
+                -e DISPLAY \
+                jamesnetherton/docker-atom-editor
+}
+
+brew:install:brew:itself() {
+	/usr/bin/ruby -e "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/master/install)"
+}

readme.md

@@ -0,0 +1,3 @@
+Clone this repository, then, on Mac OSX, run:
+
+./ci.sh

test.idr

@@ -0,0 +1,43 @@
+module Tommy
+
+data Boolean = True | False
+
+BB : Type
+BB = Boolean -> Boolean
+
+not : Boolean -> Boolean
+not True = False
+not False = True
+
+BBB : Type
+BBB = Boolean -> BB
+
+or : BBB
+or False False = False
+or _ _ = True
+
+-- mike to check out laziness and how it might relate to some of these definitions
+
+and:BBB
+and True True = True
+and _ _ = False
+
+xor:BBB
+xor True False = True
+xor False True = True
+xor _ _ = False
+
+-- natural numbers
+
+data Natural = Zero | Successor Natural
+
+naturalFromInteger : Integer -> Natural
+naturalFromInteger 0 = Zero
+naturalFromInteger n = Successor (naturalFromInteger (n - 1))
+
+integerFromNatural : Natural -> Integer
+integerFromNatural Zero = 0
+integerFromNatural (Successor n) = 1 + integerFromNatural n
+
+Show Natural where
+    show n = show (integerFromNatural n)