Initial commit.

http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html

4 files changed, 46 insertions, 0 deletions

diff --git a/DepType.idr b/DepType.idr
new file mode 100644
index 0000000..54ac7ad
--- /dev/null
+++ b/DepType.idr
@@ -0,0 +1,19 @@
+module DepType
+
+isSingleton : Bool -> Type
+isSingleton True = Nat
+isSingleton False = List Nat
+  
+sum : (single : Bool) -> isSingleton single -> Nat
+sum True x = x
+sum False (x :: xs) = x + sum False xs
+
+data MyVect : Nat -> Type -> Type where
+  Nil : MyVect Z a
+  (::) : a -> MyVect k a -> MyVect (S k) a
+
+(++) : MyVect k a -> MyVect l a -> MyVect (k + l) a
+(++) [] ys = ys
+(++) (x :: xs) ys = x :: xs ++ ys
+
+-- The finite sets.
diff --git a/Prims.idr b/Prims.idr
new file mode 100644
index 0000000..7726ca7
--- /dev/null
+++ b/Prims.idr
@@ -0,0 +1,15 @@
+module Prims
+
+x : Int
+x = 42
+
+foo : String
+foo = "Sausage machine"
+
+bar : Char
+bar = 'Z'
+
+quux : Bool
+quux = False
+  
+
diff --git a/default.nix b/default.nix
new file mode 100644
index 0000000..887dd0a
--- /dev/null
+++ b/default.nix
@@ -0,0 +1,8 @@
+with import <nixpkgs> {}; 
+
+{
+  idrisEnv = stdenv.mkDerivation {
+    name = "idris";
+    buildInputs = [ haskellPackages.idris gmp ];
+  };
+}
diff --git a/hello.idr b/hello.idr
new file mode 100644
index 0000000..bf732c8
--- /dev/null
+++ b/hello.idr
@@ -0,0 +1,4 @@
+module Main
+
+main : IO ()
+main = putStrLn "Hello, World!"