diff --git a/docs/tutorial/modules.rst b/docs/tutorial/modules.rst
index 100aed23de..55f406eebd 100644
--- a/docs/tutorial/modules.rst
+++ b/docs/tutorial/modules.rst
@@ -125,9 +125,9 @@ Idris 允许对模块内容的可见性进行细粒度的控制。默认情况
 .. - ``public export`` meaning that the entire definition is exported.
 
 - ``private`` 表示完全不被导出。这是默认的。
--
+
 - ``export`` 表示顶级类型是导出的。
--
+
 - ``public export`` 表示整个定义都是导出的。
 
 .. A further restriction in modifying the visibility is that definitions
@@ -154,9 +154,9 @@ Idris 允许对模块内容的可见性进行细粒度的控制。默认情况
 ..   long name ``public export`` is intended to make you think twice
 ..   about doing this.
 
-- ``export`` 的类型是导出的
+- ``export`` 表示导出类型
 
-- ``public export`` 的类型和定义是导出的, 在导出之后定义可被使用。
+- ``public export`` 表示导出类型和定义, 导出之后的定义可被使用。
   换言之, 定义本身被认为是模块接口的一部分。名字 ``public export``
   比较长是为了让你三思而后行。
 
@@ -400,7 +400,7 @@ API 的一部分。因此，除非你确实想要导出函数的完整定义，
 
     在数学中，对于函数 ``f(x)``，``f`` 为函数名，``x`` 则称作函数 ``f``
     的形式参数（Parameter），简称形参；在函数应用时，传输函数的参数则称作实际参数
-    （Argument），简称实参。例如 ``f(2)`` 中的 ``2`` 即为传入 ``f(x)`` 的形参。
+    （Argument），简称实参。例如 ``f(2)`` 中的 ``2`` 即为传入 ``f(x)`` 的实参。
 
     在英文原文中，有时并不明确区分形参与实参，一般统译作「参数」。只有当需要明确区分时，
     才分别译作「形参」与「实参」。
diff --git a/docs/tutorial/theorems.rst b/docs/tutorial/theorems.rst
index 4603258de6..8356ec1b52 100644
--- a/docs/tutorial/theorems.rst
+++ b/docs/tutorial/theorems.rst
@@ -209,7 +209,7 @@ to look something like the following:
 
 Unfortunately, this fails with a type error:
 
-不幸的是，它会因类型错误而失败：
+不幸的是，它会因类型错误而无法通过编译：
 
 ::
 
diff --git a/docs/tutorial/typesfuns.rst b/docs/tutorial/typesfuns.rst
index 1388cf4344..5ca95353c2 100644
--- a/docs/tutorial/typesfuns.rst
+++ b/docs/tutorial/typesfuns.rst
@@ -1011,7 +1011,7 @@ IO 操作中：
 .. itself (that is, Idris uses *eager* evaluation). However, this is
 .. not always the best approach. Consider the following function:
 
-通常，函数的参数会在函数之前求值（也就是说，Idris 采用了 **及早** 求值）。
+通常，函数的参数会在函数之前求值（也就是说，Idris 采用了 **及早（Eager）** 求值）。
 然而，这并不总是最佳方式。考虑以下函数：
 
 .. code-block:: idris
@@ -1102,7 +1102,7 @@ Idris 提供了 ``Lazy`` 数据类型，它允许延缓求值：
 .. mutually recursive data structures. For example the following will create an
 .. infinite loop and cause a stack overflow.
 
-要重点注意：codata 不允许创建无穷互用的递归数据结构。
+要重点注意：余数据类型不允许创建无穷互用的递归数据结构。
 例如，以下代码会创建一个无穷循环并导致栈溢出：
 
 .. code-block:: idris
@@ -1133,7 +1133,7 @@ Idris 提供了 ``Lazy`` 数据类型，它允许延缓求值：
 .. **different** type from the one being defined. For example, the following
 .. outputs "1".
 
-为了修复它，我们必须为构造器参数的类型显式地加上 ``Inf`` 声明，因为 codata
+为了修复它，我们必须为构造器参数的类型显式地加上 ``Inf`` 声明，因为余数据类型
 不会将它添加到与正在定义的构造器类型 **不同** 的构造器参数上。例如，以下程序输出「1」。
 
 .. code-block:: idris
@@ -1164,10 +1164,10 @@ Idris 提供了 ``Lazy`` 数据类型，它允许延缓求值：
 
 .. hint:: 「归纳数据类型」和「余归纳数据类型」
 
-    余数据类型（codata type）的全称为余归纳数据类型（coinductive data type），
+    余数据类型（Codata Type）的全称为余归纳数据类型（Coinductive Data Type），
     归纳数据类型和余归纳数据类型是对偶的关系。从语义上看，
-    inductive type 描述了如何从更小的 term 构造成更大的 term；而
-    coinductive type 则描述了如何从更大的 term 分解成更小的 term。
+    Inductive Type 描述了如何从更小的 term 构造成更大的 term；而
+    Coinductive Type 则描述了如何从更大的 term 分解成更小的 term。
     —— `Belleve <https://www.zhihu.com/question/60184579/answer/255291675>`_
 
 
@@ -1291,7 +1291,7 @@ Idris 包含了很多常用的数据类型和库函数（见发行版中的 ``li
 .. There are actually neater ways to write the above expression. One way
 .. would be to use an anonymous function:
 
-上面的表达式其实还有更加利落的写法。其中一种就是使用匿名函数（anonymous function）：
+上面的表达式其实还有更加利落的写法。其中一种就是使用匿名函数（Anonymous Function）：
 
 ::
 
@@ -1322,7 +1322,7 @@ Idris 包含了很多常用的数据类型和库函数（见发行版中的 ``li
 ``(*2)`` 是将数字乘以 2 的函数的简写，它会被展开为 ``\x => x * 2``。
 同样，``(2*)`` 会被展开为 ``\x => 2 * x``。
 
-.. hint:: 匿名函数在函数式编程中又称为 λ-表达式（lambda expression）。
+.. hint:: 匿名函数在函数式编程中又称为 λ-表达式（Lambda Expression）。
 
 Maybe
 -----