diff --git a/ci.sh b/ci.sh new file mode 100644 index 0000000..1218f01 --- /dev/null +++ b/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)" +} \ No newline at end of file diff --git a/readme.md b/readme.md new file mode 100644 index 0000000..428c631 --- /dev/null +++ b/readme.md @@ -0,0 +1,3 @@ +Clone this repository, then, on Mac OSX, run: + +./ci.sh \ No newline at end of file diff --git a/test.ibc b/test.ibc new file mode 100644 index 0000000..4a3f34c Binary files /dev/null and b/test.ibc differ diff --git a/test.idr b/test.idr new file mode 100644 index 0000000..b42c186 --- /dev/null +++ b/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)