Copy samples directory from Idris2-boot

This is referred to in the documentation, so should be there

samples/BTree.idr

@@ -0,0 +1,21 @@
+module BTree
+
+public export
+data BTree a = Leaf
+             | Node (BTree a) a (BTree a)
+
+export
+insert : Ord a => a -> BTree a -> BTree a
+insert x Leaf = Node Leaf x Leaf
+insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
+                                   else (Node l v (insert x r))
+
+export
+toList : BTree a -> List a
+toList Leaf = []
+toList (Node l v r) = BTree.toList l ++ (v :: BTree.toList r)
+
+export
+toTree : Ord a => List a -> BTree a
+toTree [] = Leaf
+toTree (x :: xs) = insert x (toTree xs)

samples/FFI-readline/Test/ReadHistory.idr

@@ -0,0 +1,14 @@
+import Text.Readline
+
+echoLoop : IO ()
+echoLoop
+    = do Just x <- readline "> "
+              | Nothing => putStrLn "EOF"
+         putStrLn ("Read: " ++ x)
+         when (x /= "") $ addHistory x
+         if x /= "quit"
+            then echoLoop
+            else putStrLn "Done"
+
+main : IO ()
+main = echoLoop

samples/FFI-readline/Test/ReadTab.idr

@@ -0,0 +1,19 @@
+import Text.Readline
+
+testComplete : String -> Int -> IO (Maybe String)
+testComplete text 0 = pure $ Just "hamster"
+testComplete text 1 = pure $ Just "bar"
+testComplete text st = pure Nothing
+
+loop : IO ()
+loop = do Just x <- readline "> "
+               | Nothing => putStrLn "EOF"
+          putStrLn x
+          when (x /= "") $ addHistory x
+          if x /= "quit"
+             then loop
+             else putStrLn "Done"
+
+main : IO ()
+main = do setCompletionFn testComplete
+          loop

samples/FFI-readline/Test/test.ipkg

@@ -0,0 +1,3 @@
+package test
+
+opts = "-p readline"

samples/FFI-readline/readline.ipkg

@@ -0,0 +1,10 @@
+package readline
+
+sourcedir = "src"
+
+modules = Text.Readline
+
+prebuild = "make -C readline_glue"
+postinstall = "make -C readline_glue install"
+postclean = "make -C readline_glue clean"
+

samples/FFI-readline/readline_glue/.gitignore

@@ -0,0 +1,7 @@
+*.d
+*.o
+*.obj
+*.so
+*.dylib
+*.dll
+

samples/FFI-readline/readline_glue/Makefile

@@ -0,0 +1,40 @@
+include ../../../config.mk
+
+IDRIS := idris2
+INSTALLDIR = `${IDRIS} --libdir`/readline/lib
+
+TARGET = libidrisreadline
+
+LDFLAGS += -lreadline
+
+SRCS = $(wildcard *.c)
+OBJS = $(SRCS:.c=.o)
+DEPS = $(OBJS:.o=.d)
+
+
+all: $(TARGET)$(SHLIB_SUFFIX)
+
+$(TARGET)$(SHLIB_SUFFIX): $(OBJS)
+	$(CC) -shared $(LDFLAGS) -o $@ $^
+
+
+-include $(DEPS)
+
+%.d: %.c
+	@$(CPP) $(CFLAGS) $< -MM -MT $(@:.d=.o) >$@
+
+
+.PHONY: clean
+
+clean :
+	rm -f $(OBJS) $(TARGET)$(SHLIB_SUFFIX)
+
+cleandep: clean
+	rm -f $(DEPS)
+
+
+.PHONY: install
+
+install:
+	@if ! [ -d $(INSTALLDIR) ]; then mkdir -p $(INSTALLDIR); fi
+	install $(TARGET)$(SHLIB_SUFFIX) $(wildcard *.h) $(INSTALLDIR)

samples/FFI-readline/readline_glue/idris_readline.c

@@ -0,0 +1,38 @@
+#include <readline/readline.h>
+#include <string.h>
+#include <stdlib.h>
+
+rl_compentry_func_t* my_compentry;
+
+char* compentry_wrapper(const char* text, int i) {
+    char* res = my_compentry(text, i); // Idris frees this
+    if (res != NULL) {
+        char* comp = malloc(strlen(res)+1); // Readline frees this
+        strcpy(comp, res);
+        return comp;
+    }
+    else {
+        return NULL;
+    }
+}
+
+void idrisrl_setCompletion(rl_compentry_func_t* fn) {
+    rl_completion_entry_function = compentry_wrapper;
+    my_compentry = fn;
+}
+
+char* getString(void* str) {
+    return (char*)str;
+}
+
+void* mkString(char* str) {
+    return (void*)str;
+}
+
+void* nullString() {
+    return NULL;
+}
+
+int isNullString(void* str) {
+    return str == NULL;
+}

samples/FFI-readline/readline_glue/idris_readline.h

@@ -0,0 +1,11 @@
+#ifndef _IDRIS_READLINE_H
+#define _IDRIS_READLINE_H
+
+void idrisrl_setCompletion(rl_completion_func_t* fn);
+
+char* getString(void* str);
+void* mkString(char* str);
+void* nullString();
+int isNullString(void* str);
+
+#endif

samples/FFI-readline/src/Text/Readline.idr

@@ -0,0 +1,53 @@
+module Text.Readline
+
+rlib : String -> String
+rlib fn = "C:" ++ fn ++ ",libidrisreadline"
+
+%foreign (rlib "getString")
+export
+getString : Ptr String -> String
+
+%foreign (rlib "mkString")
+export
+mkString : String -> Ptr String
+
+%foreign (rlib "nullString")
+export
+nullString : Ptr String
+
+%foreign (rlib "isNullString")
+prim_isNullString : Ptr String -> Int
+
+export
+isNullString : Ptr String -> Bool
+isNullString str = if prim_isNullString str == 0 then False else True
+
+%foreign (rlib "readline")
+prim_readline : String -> PrimIO (Ptr String)
+
+export
+readline : HasIO io => String -> io (Maybe String)
+readline s
+    = do mstr <- primIO $ prim_readline s
+         if isNullString mstr
+            then pure $ Nothing
+            else pure $ Just (getString mstr)
+
+%foreign (rlib "add_history")
+prim_add_history : String -> PrimIO ()
+
+export
+addHistory : HasIO io => String -> io ()
+addHistory s = primIO $ prim_add_history s
+
+%foreign (rlib "idrisrl_setCompletion")
+prim_setCompletion : (String -> Int -> PrimIO (Ptr String)) -> PrimIO ()
+
+export
+setCompletionFn : HasIO io => (String -> Int -> IO (Maybe String)) -> io ()
+setCompletionFn fn
+    = primIO $ prim_setCompletion $ \s, i => toPrim $
+          do mstr <- fn s i
+             case mstr of
+                  Nothing => pure nullString
+                  Just str => pure (mkString str)

samples/Interp.idr

@@ -0,0 +1,57 @@
+import Data.Vect
+
+data Ty = TyInt | TyBool | TyFun Ty Ty
+
+interpTy : Ty -> Type
+interpTy TyInt       = Integer
+interpTy TyBool      = Bool
+interpTy (TyFun a t) = interpTy a -> interpTy t
+
+data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
+    Stop : HasType FZ (t :: ctxt) t
+    Pop  : HasType k ctxt t -> HasType (FS k) (u :: ctxt) t
+
+data Expr : Vect n Ty -> Ty -> Type where
+    Var : HasType i ctxt t -> Expr ctxt t
+    Val : (x : Integer) -> Expr ctxt TyInt
+    Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t)
+    App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t
+    Op  : (interpTy a -> interpTy b -> interpTy c) ->
+          Expr ctxt a -> Expr ctxt b -> Expr ctxt c
+    If  : Expr ctxt TyBool ->
+          Lazy (Expr ctxt a) ->
+          Lazy (Expr ctxt a) -> Expr ctxt a
+
+data Env : Vect n Ty -> Type where
+    Nil  : Env Nil
+    (::) : interpTy a -> Env ctxt -> Env (a :: ctxt)
+
+lookup : HasType i ctxt t -> Env ctxt -> interpTy t
+lookup Stop    (x :: xs) = x
+lookup (Pop k) (x :: xs) = lookup k xs
+
+interp : Env ctxt -> Expr ctxt t -> interpTy t
+interp env (Var i)     = lookup i env
+interp env (Val x)     = x
+interp env (Lam sc)    = \x => interp (x :: env) sc
+interp env (App f s)   = interp env f (interp env s)
+interp env (Op op x y) = op (interp env x) (interp env y)
+interp env (If x t e)  = if interp env x then interp env t
+                                         else interp env e
+
+add : Expr ctxt (TyFun TyInt (TyFun TyInt TyInt))
+add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
+
+fact : Expr ctxt (TyFun TyInt TyInt)
+fact = Lam (If (Op (==) (Var Stop) (Val 0))
+               (Val 1)
+               (Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
+                       (Var Stop)))
+
+main : IO ()
+main = do putStr "Enter a number: "
+          x <- getLine
+          printLn (interp [] fact (cast x))
+
+
+

samples/InterpE.idr

@@ -0,0 +1,36 @@
+module InterpE
+
+data Expr = Var String      -- variables
+          | Val Int         -- values
+          | Add Expr Expr   -- addition
+
+data Eval : Type -> Type where
+     MkEval : (List (String, Int) -> Maybe a) -> Eval a
+
+fetch : String -> Eval Int
+fetch x = MkEval (\e => fetchVal e) where
+    fetchVal : List (String, Int) -> Maybe Int
+    fetchVal [] = Nothing
+    fetchVal ((v, val) :: xs) = if (x == v)
+                                  then (Just val)
+                                  else (fetchVal xs)
+
+Functor Eval where
+    map f (MkEval g) = MkEval (\e => map f (g e))
+
+Applicative Eval where
+    pure x = MkEval (\e => Just x)
+
+    (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
+        app : Maybe (a -> b) -> Maybe a -> Maybe b
+        app (Just fx) (Just gx) = Just (fx gx)
+        app _         _         = Nothing
+
+eval : Expr -> Eval Int
+eval (Var x)   = fetch x
+eval (Val x)   = [| x |]
+eval (Add x y) = [| eval x + eval y |]
+
+runEval : List (String, Int) -> Expr -> Maybe Int
+runEval env e = case eval e of
+    MkEval envFn => envFn env

samples/MyOrd.idr

@@ -0,0 +1,10 @@
+import Data.List
+
+[myord] Ord Nat where
+   compare Z (S n)     = GT
+   compare (S n) Z     = LT
+   compare Z Z         = EQ
+   compare (S x) (S y) = compare @{myord} x y
+
+testList : List Nat
+testList = [3,4,1]

samples/NamedSemi.idr

@@ -0,0 +1,11 @@
+[PlusNatSemi] Semigroup Nat where
+  (<+>) x y = x + y
+
+[MultNatSemi] Semigroup Nat where
+  (<+>) x y = x * y
+
+[PlusNatMonoid] Monoid Nat using PlusNatSemi where
+  neutral = 0
+
+[MultNatMonoid] Monoid Nat using MultNatSemi where
+  neutral = 1

samples/Prims.idr

@@ -0,0 +1,13 @@
+module Prims
+
+x : Int
+x = 94
+
+foo : String
+foo = "Sausage machine"
+
+bar : Char
+bar = 'Z'
+
+quux : Bool
+quux = False

samples/Proofs.idr

@@ -0,0 +1,29 @@
+fiveIsFive : 5 = 5
+fiveIsFive = Refl
+
+twoPlusTwo : 2 + 2 = 4
+twoPlusTwo = Refl
+
+-- twoPlusTwoBad : 2 + 2 = 5
+-- twoPlusTwoBad = Refl
+
+disjoint : (n : Nat) -> Z = S n -> Void
+disjoint n prf = replace {p = disjointTy} prf ()
+  where
+    disjointTy : Nat -> Type
+    disjointTy Z = ()
+    disjointTy (S k) = Void
+
+plusReduces : (n:Nat) -> plus Z n = n
+plusReduces n = Refl
+
+plusReducesR : (n:Nat) -> plus n Z = n
+plusReducesR n = Refl
+
+plusReducesZ : (n:Nat) -> n = plus n Z
+plusReducesZ Z = Refl
+plusReducesZ (S k) = cong S (plusReducesZ k)
+
+plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
+plusReducesS Z m = Refl
+plusReducesS (S k) m = cong S (plusReducesS k m)

samples/Vect.idr

@@ -0,0 +1,40 @@
+data Vect : Nat -> Type -> Type where
+   Nil  : Vect Z a
+   (::) : a -> Vect k a -> Vect (S k) a
+
+(++) : Vect n a -> Vect m a -> Vect (n + m) a
+(++) Nil       ys = ys
+(++) (x :: xs) ys = x :: xs ++ ys
+
+data Fin : Nat -> Type where
+   FZ : Fin (S k)
+   FS : Fin k -> Fin (S k)
+
+index : Fin n -> Vect n a -> a
+index FZ     (x :: xs) = x
+index (FS k) (x :: xs) = index k xs
+
+filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
+filter p Nil = (_ ** [])
+filter p (x :: xs)
+    = case filter p xs of
+           (_ ** xs') => if p x then (_ ** x :: xs')
+                                else (_ ** xs')
+
+cons : t -> (x : Nat ** Vect x t) -> (x : Nat ** Vect x t)
+cons val xs
+    = record { fst = S (fst xs),
+               snd = (val :: snd xs) } xs
+
+cons' : t -> (x : Nat ** Vect x t) -> (x : Nat ** Vect x t)
+cons' val
+    = record { fst $= S,
+               snd $= (val ::) }
+
+Show a => Show (Vect n a) where
+    show xs = "[" ++ show' xs ++ "]" where
+        show' : forall n . Vect n a -> String
+        show' Nil        = ""
+        show' (x :: Nil) = show x
+        show' (x :: xs)  = show x ++ ", " ++ show' xs
+

samples/Void.idr

@@ -0,0 +1,11 @@
+module Void
+
+-- making use of 'hd' being partially defined
+empty1 : Void
+empty1 = hd [] where
+    hd : List a -> a
+    hd (x :: xs) = x
+
+-- not terminating
+empty2 : Void
+empty2 = empty2

samples/With.idr

@@ -0,0 +1,47 @@
+import Data.Vect
+import Data.Nat
+
+my_filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
+my_filter p [] = ( _ ** [] )
+my_filter p (x :: xs) with (filter p xs)
+  my_filter p (x :: xs) | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
+
+foo : Int -> Int -> Bool
+foo n m with (n + 1)
+  foo _ m | 2 with (m + 1)
+    foo _ _ | 2 | 3 = True
+    foo _ _ | 2 | _ = False
+  foo _ _ | _ = False
+
+data Parity : Nat -> Type where
+     Even : {n : _} -> Parity (n + n)
+     Odd  : {n : _} ->Parity (S (n + n))
+
+-- parity : (n : Nat) -> Parity n
+-- parity Z = Even {n = Z}
+-- parity (S Z) = Odd {n = Z}
+-- parity (S (S k)) with (parity k)
+--   parity (S (S (j + j))) | Even
+--       = rewrite plusSuccRightSucc j j in Even {n = S j}
+--   parity (S (S (S (j + j)))) | Odd
+--       = rewrite plusSuccRightSucc j j in Odd {n = S j}
+
+helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
+helpEven j p = rewrite plusSuccRightSucc j j in p
+
+helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))
+helpOdd j p = rewrite plusSuccRightSucc j j in p
+
+parity : (n:Nat) -> Parity n
+parity Z     = Even {n=Z}
+parity (S Z) = Odd {n=Z}
+parity (S (S k)) with (parity k)
+  parity (S (S (j + j)))     | Even = helpEven j (Even {n = S j})
+  parity (S (S (S (j + j)))) | Odd  = helpOdd j (Odd {n = S j})
+        
+natToBin : Nat -> List Bool
+natToBin Z = Nil
+natToBin k with (parity k)
+   natToBin (j + j)     | Even = False :: natToBin j
+   natToBin (S (j + j)) | Odd  = True  :: natToBin j
+

samples/bmain.idr

@@ -0,0 +1,7 @@
+module Main
+
+import BTree
+
+main : IO ()
+main = do let t = toTree [1,8,2,7,9,3]
+          print (BTree.toList t)

samples/deprec.idr

@@ -0,0 +1,25 @@
+import Data.Vect
+
+record Person where
+    constructor MkPerson
+    firstName, middleName, lastName : String
+    age : Int
+
+record SizedClass (size : Nat) where
+    constructor SizedClassInfo
+    students : Vect size Person
+    className : String
+
+record Class where
+    constructor ClassInfo
+    students : Vect n Person
+    className : String
+
+addStudent : Person -> Class -> Class
+addStudent p c = record { students = p :: students c } c
+
+addStudent' : Person -> SizedClass n -> SizedClass (S n)
+addStudent' p c =  SizedClassInfo (p :: students c) (className c)
+
+addStudent'' : Person -> SizedClass n -> SizedClass (S n)
+addStudent'' p c = record { students = p :: students c } c

samples/dummy.ipkg

@@ -0,0 +1,5 @@
+-- This is just so the above Idris 1 ipkg doesn't interfere with the
+-- interactive editing modes for the Idris 2 code here!
+
+package dummy
+

samples/fctypes.idr

@@ -0,0 +1,13 @@
+
+isSingleton : Bool -> Type
+isSingleton True = Nat
+isSingleton False = List Nat
+
+mkSingle : (x : Bool) -> isSingleton x
+mkSingle True = 0
+mkSingle False = []
+
+sum : (single : Bool) -> isSingleton single -> Nat
+sum True x = x
+sum False [] = 0
+sum False (x :: xs) = x + sum False xs

samples/ffi/Small.idr

@@ -0,0 +1,40 @@
+libsmall : String -> String
+libsmall fn = "C:" ++ fn ++ ",libsmall"
+
+%foreign (libsmall "add")
+add : Int -> Int -> Int
+
+%foreign (libsmall "addWithMessage")
+prim_addWithMessage : String -> Int -> Int -> PrimIO Int
+
+addWithMessage : String -> Int -> Int -> IO Int
+addWithMessage s x y = primIO $ prim_addWithMessage s x y
+
+%foreign (libsmall "applyFn")
+prim_applyFn : String -> Int -> (String -> Int -> String) -> PrimIO String
+
+applyFn : String -> Int -> (String -> Int -> String) -> IO String
+applyFn c i f = primIO $ prim_applyFn c i f
+
+%foreign (libsmall "applyFn")
+prim_applyFnIO : String -> Int -> (String -> Int -> PrimIO String) -> PrimIO String
+
+applyFnIO : String -> Int -> (String -> Int -> IO String) -> IO String
+applyFnIO c i f = primIO $ prim_applyFnIO c i (\s, i => toPrim $ f s i)
+
+pluralise : String -> Int -> IO String
+pluralise str x
+    = do putStrLn "Pluralising"
+         pure $ show x ++ " " ++
+                if x == 1
+                   then str
+                   else str ++ "s"
+
+main : IO ()
+main
+    = do -- printLn (add 70 24)
+         -- primIO $ prim_addWithMessage "Sum" 70 24
+         str1 <- applyFnIO "Biscuit" 10 pluralise
+         putStrLn str1
+         str2 <- applyFnIO "Tree" 1 pluralise
+         putStrLn str2

samples/ffi/Struct.idr

@@ -0,0 +1,29 @@
+import System.FFI
+
+libsmall : String -> String
+libsmall fn = "C:" ++ fn ++ ",libsmall"
+
+Point : Type
+Point = Struct "point" [("x", Int), ("y", Int)]
+
+%foreign (libsmall "mkPoint")
+mkPoint : Int -> Int -> Point
+
+%foreign (libsmall "freePoint")
+prim_freePoint : Point -> PrimIO ()
+
+freePoint : Point -> IO ()
+freePoint p = primIO $ prim_freePoint p
+
+showPoint : Point -> String
+showPoint pt
+    = let x : Int = getField pt "x"
+          y : Int = getField pt "y" in
+          show (x, y)
+
+main : IO ()
+main
+    = do let pt = mkPoint 20 30
+         setField pt "x" (the Int 40)
+         putStrLn $ showPoint pt
+         freePoint pt

samples/ffi/args.idr

@@ -0,0 +1,4 @@
+import System
+
+main : IO ()
+main = printLn !getArgs

samples/ffi/dummy.ipkg

@@ -0,0 +1,5 @@
+-- This is just so the above Idris 1 ipkg doesn't interfere with the
+-- interactive editing modes for the Idris 2 code here!
+
+package dummy
+

samples/ffi/smallc.c

@@ -0,0 +1,39 @@
+#include <stdlib.h>
+#include <stdio.h>
+
+int add(int x, int y) {
+    return x+y;
+}
+
+int addWithMessage(char* msg, int x, int y) {
+    printf("%s: %d + %d = %d\n", msg, x, y, x+y);
+    return x+y;
+}
+
+typedef char*(*StringFn)(char*, int);
+
+char* applyFn(char* x, int y, StringFn f) {
+    printf("Applying callback to %s %d\n", x, y);
+    return f(x, y);
+}
+
+char* applyFnPure(char* x, int y, StringFn f) {
+    return f(x, y);
+}
+
+typedef struct {
+    int x;
+    int y;
+} point;
+
+point* mkPoint(int x, int y) {
+    point* pt = malloc(sizeof(point));
+    pt->x = x;
+    pt->y = y;
+    return pt;
+}
+
+void freePoint(point* pt) {
+    free(pt);
+}
+

samples/holes.idr

@@ -0,0 +1,6 @@
+main : IO ()
+main = putStrLn ?greeting
+
+even : Nat -> Bool
+even Z = True
+even (S k) = ?even_rhs

samples/io.idr

@@ -0,0 +1,4 @@
+greet : IO ()
+greet = do putStr "What is your name? "
+           name <- getLine
+           putStrLn ("Hello " ++ name)

samples/listcomp.idr

@@ -0,0 +1,3 @@
+pythag : Int -> List (Int, Int, Int)
+pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
+                         x*x + y*y == z*z ]

samples/multiplicity.idr

@@ -0,0 +1,22 @@
+import Data.Vect
+
+append : Vect n a -> Vect m a -> Vect (n + m) a
+append xs ys = ?append_rhs
+
+data DoorState = Open | Closed
+
+data Door : DoorState -> Type where
+     MkDoor : (doorId : Int) -> Door st
+
+openDoor : (1 d : Door Closed) -> Door Open
+closeDoor : (1 d : Door Open) -> Door Closed
+
+newDoor : (1 p : (1 d : Door Closed) -> IO ()) -> IO ()
+deleteDoor : (1 d : Door Closed) -> IO ()
+
+doorProg : IO ()
+doorProg
+    = newDoor $ \d =>
+          let d' = openDoor d
+              d'' = closeDoor d' in
+              deleteDoor d''

samples/params.idr

@@ -0,0 +1,12 @@
+import Data.Vect
+
+parameters (x : Nat, y : Nat)
+  addAll : Nat -> Nat
+  addAll z = x + y + z
+
+parameters (y : Nat, xs : Vect x a)
+  data Vects : Type -> Type where
+    MkVects : Vect y a -> Vects a
+
+  append : Vects a -> Vect (x + y) a
+  append (MkVects ys) = xs ++ ys

samples/proofs/induction.idr

@@ -0,0 +1,17 @@
+nat_induction : 
+    (prop : Nat -> Type) ->                -- Property to show
+    (prop Z) ->                            -- Base case
+    ((k : Nat) -> prop k -> prop (S k)) -> -- Inductive step
+    (x : Nat) ->                           -- Show for all x
+    prop x
+nat_induction prop p_Z p_S Z = p_Z
+nat_induction prop p_Z p_S (S k) = p_S k (nat_induction prop p_Z p_S k)
+
+plus_ind : Nat -> Nat -> Nat
+plus_ind n m
+   = nat_induction (\x => Nat)
+                   m                      -- Base case, plus_ind Z m
+                   (\k, k_rec => S k_rec) -- Inductive step plus_ind (S k) m
+                                          -- where k_rec = plus_ind k m
+                   n
+

samples/proofs/pluscomm.idr

@@ -0,0 +1,17 @@
+plus_commutes_Z : (m : Nat) -> m = plus m Z
+plus_commutes_Z Z = Refl
+plus_commutes_Z (S k)
+   = let rec = plus_commutes_Z k in
+         rewrite sym rec in Refl
+
+plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
+plus_commutes_S k Z = Refl
+plus_commutes_S k (S j)
+   = rewrite plus_commutes_S k j in Refl
+
+total
+plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
+plus_commutes Z m = plus_commutes_Z m
+plus_commutes (S k) m 
+    = rewrite plus_commutes k m in
+              plus_commutes_S k m

samples/proofs/plusprops.idr

@@ -0,0 +1,4 @@
+plus_commutes : (n, m : Nat) -> plus n m = plus m n
+plus_assoc : (n, m, p : Nat) -> plus n (plus m p) = plus (plus n m) p
+
+

samples/proofs/prfintro.idr

@@ -0,0 +1,21 @@
+import Data.Vect
+
+four_eq : 4 = 4
+four_eq = Refl
+
+-- four_eq_five : 4 = 5
+-- four_eq_five = Refl
+
+twoplustwo_eq_four : 2 + 2 = 4
+twoplustwo_eq_four = Refl
+
+plus_reduces_Z : (m : Nat) -> plus Z m = m
+plus_reduces_Z m = Refl
+
+plus_reduces_Sk : (k, m : Nat) -> plus (S k) m = S (plus k m)
+plus_reduces_Sk k m = Refl
+
+idris_not_php : Z = "Z"
+
+vect_eq_length : (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> n = m
+vect_eq_length xs xs Refl = Refl

samples/proofs/proof.ipkg

@@ -0,0 +1,5 @@
+-- This is just so the above ipkg doesn't interfere with the
+-- interactive editing modes for the Idris 2 code here!
+
+package proof
+

samples/wheres.idr

@@ -0,0 +1,26 @@
+foo : Int -> Int
+foo x = case isLT of
+            Yes => x*2
+            No => x*4
+    where
+       data MyLT = Yes | No
+
+       isLT : MyLT
+       isLT = if x < 20 then Yes else No
+
+even : Nat -> Bool
+even Z = True
+even (S k) = odd k where
+  odd : Nat -> Bool
+  odd Z = False
+  odd (S k) = even k
+
+test : List Nat
+test = [c (S 1), c Z, d (S Z)]
+  where c : Nat -> Nat
+        c x = 42 + x
+
+        d : Nat -> Nat
+        d y = c (y + 1 + z y)
+              where z : Nat -> Nat
+                    z w = y + w