added link to slides

Author: sweirich

README.md

@@ -2,19 +2,23 @@ Pi-Forall language
 ------------------
 
 This language implementation is designed to accompany four lectures at
-OPLSS during Summer 2014. Notes for these lectures are available at:
+OPLSS during Summer 2014. Notes for these lectures are included in the 
+distribution:
 
 - [notes.md](notes.md):    Basic language with Type:Type 
 - [notes2.md](notes2.md):  Implementation of basic languages
 - [notes3.md](notes3.md):  Definitional and propositional equality
 - [notes4.md](notes4.md):  Datatypes, with parameters and indices, erased arguments
 
-Each set of lecture notes corresponds to an increasingly expressive demo
+Videos for these lectures are also available from the 
+[OPLSS website](https://www.cs.uoregon.edu/research/summerschool/summer14/curriculum.html).
+
+These lecture notes corresponds to an increasingly expressive demo
 implementation of dependently-typed lambda calculus.
 
 - [version1/](version1/):   Basic language implementation, 
-- [version2/](version2/):   Language extended with nontrivial definitional equality
-- [soln/](soln/):           Language with datatypes and erased arguments
+- [version2/](version2/):   Basic language extended with nontrivial definitional equality
+- [soln/](soln/):           Full language with datatypes and erased arguments
 
 See also the implementation [README.md](master/README.md) for more details.
 

master/README.md

@@ -25,11 +25,11 @@ Features
   - bidirectional type checking
   - erased arguments (forall)
   - propositional equality 
-  - inductive & indexed datatypes 
+  - indexed datatypes 
 
 Not covered (Future work!)
 --------------------------
-  - nontermination
+  - termination & inductive datatypes
   - effects
   - co-induction
   - type inference & unification