Merge branch 'develop' into logic

Author: Alex Gryzlov

software_foundations.ipkg

@@ -4,6 +4,7 @@ modules    = Basics
            , Induction
            , Lists
            , Poly
+           , Tactics
 
 brief      = "Software Foundations in Idris"
 version    = 0.0.1.0
@@ -18,4 +19,4 @@ sourceloc  = git://[email protected]:idris-hackers/software-foundations.git
 bugtracker = https://github.com/idris-hackers/software-foundations/issues
 
 sourcedir  = src
-opts       = "--check --total"
+opts       = "--check --total -p pruviloj"

src/Makefile

@@ -15,7 +15,8 @@ LIDR_FILES := Preface.lidr \
 	Basics.lidr \
 	Induction.lidr \
 	Lists.lidr \
-	Poly.lidr
+	Poly.lidr \
+	Tactics.lidr
 # TODO: Add more chapters, in order, here.
 
 

src/Poly.lidr

@@ -293,7 +293,7 @@ polymorphic lists...
 > app Nil l2 = l2
 > app (h::t) l2 = h :: app t l2
 
-> rev : (l: List x) -> List x
+> rev : (l : List x) -> List x
 > rev [] = []
 > rev (h::t) = app (rev t) (h::Nil)