Added lecture 3 notes and code

Author: edwinb

Code/Lecture3/Exercise.txt

@@ -0,0 +1,7 @@
+Today's exercise:
+
+There are some holes in this version of TTImp.Elab.Term, in the rules for
+Pi and Lambda. Fill them in by following the typing rules.
+
+You can find some of the answers in TinyIdris-v1. But there is also a hole 
+for a Lambda with an unknown expected type. How can you handle this?

Code/Lecture3/TinyIdris-v1/Test/Nat.tidr

@@ -0,0 +1,9 @@
+data Nat : Type where
+     Z : Nat
+     S : Nat -> Nat
+
+plus : Nat -> Nat -> Nat
+pat y : Nat =>
+   plus Z y = y
+pat k : Nat, y : Nat =>
+   plus (S k) y = S (plus k y)

Code/Lecture3/TinyIdris-v1/Test/Vect.tidr

@@ -0,0 +1,22 @@
+data Nat : Type where
+     Z : Nat
+     S : Nat -> Nat
+
+plus : Nat -> Nat -> Nat
+pat y : Nat =>
+   plus Z y = y
+pat k : Nat, y : Nat =>
+   plus (S k) y = S (plus k y)
+
+data Vect : Nat -> Type -> Type where
+     Nil : (a : Type) -> Vect Z a
+     Cons : (a : Type) -> (k : Nat) ->
+            a -> Vect k a -> Vect (S k) a
+
+append : (a : Type) -> (n : Nat) -> (m : Nat) ->
+         Vect n a -> Vect m a -> Vect (plus n m) a
+pat a : Type, k : Nat, ys : Vect k a =>
+    append a Z k (Nil a) ys = ys
+pat a : Type, n : Nat, x : a, xs : Vect n a, k : Nat, ys : Vect k a =>
+    append a (S n) k (Cons a n x xs) ys
+        = Cons a (plus n k) x (append a n k xs ys)