From 28fe6d4bb1df0fbdb84e9a2bdb8106e60fbfe2bf Mon Sep 17 00:00:00 2001
From: Andrew Kent <andmkent@iu.edu>
Date: Mon, 5 Mar 2018 15:37:29 -0500
Subject: [PATCH] fix ind-List doc typo

---
 pie.scrbl | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/pie.scrbl b/pie.scrbl
index c542a02..e9a989a 100644
--- a/pie.scrbl
+++ b/pie.scrbl
@@ -303,8 +303,8 @@ The second projection of a pair. If @pie[p] is a @pie[(Σ ((_x _A)) _D)], then
                            [base (motive nil)]
                            [step (Π ((e _E)
                                      (es (List _E)))
-                                   (-> (mot es)
-                                     (mot (:: e es))))])
+                                   (-> (motive es)
+                                     (motive (:: e es))))])
                  (motive target)]{
  @pie[ind-List] is induction on lists. When @pie[target] is a @pie[(List _E)], t
  the whole expression's type is @pie[(motive target)], the type of