多态：翻译完毕

.gitignore

@@ -3,3 +3,4 @@ functional-programming-lean/book
 *#
 .#*
 *.olean
+.vscode

functional-programming-lean/book.toml

@@ -7,6 +7,9 @@ title = "Functional Programming in Lean"
 
 [build]
 
+[preprocessor.gettext]
+after = ["links"]
+
 [preprocessor.buildexamples]
 command = "python -X utf8 scripts/build-examples.py"
 before = ["leanexample", "commands"]
@@ -20,8 +23,6 @@ command = "python -X utf8 scripts/projects.py"
 [preprocessor.leanversion]
 command = "python -X utf8 scripts/lean-version.py"
 
-[preprocessor.gettext]
-after = ["links"]
 
 [output.html]
 additional-css = ["custom.css", "pygments.css"]

functional-programming-lean/src/SUMMARY.md

@@ -1,73 +1,73 @@
-# Functional Programming in Lean
+# Lean 函数式编程
 
-[Functional Programming in Lean](./title.md)
-[Introduction](./introduction.md)
-[Acknowledgments](./acknowledgments.md)
+[Lean 函数式编程](./title.md)
+[引言](./introduction.md)
+[致谢](./acknowledgments.md)
 
-- [Getting to Know Lean](./getting-to-know.md)
-  - [Evaluating Expressions](./getting-to-know/evaluating.md)
-  - [Types](./getting-to-know/types.md)
-  - [Functions and Definitions](./getting-to-know/functions-and-definitions.md)
-  - [Structures](./getting-to-know/structures.md)
-  - [Datatypes, Patterns and Recursion](./getting-to-know/datatypes-and-patterns.md)
-  - [Polymorphism](./getting-to-know/polymorphism.md)
-  - [Additional Conveniences](./getting-to-know/conveniences.md)
-  - [Summary](./getting-to-know/summary.md)
+- [了解 Lean](./getting-to-know.md)
+  - [求值表达式](./getting-to-know/evaluating.md)
+  - [类型](./getting-to-know/types.md)
+  - [函数与定义](./getting-to-know/functions-and-definitions.md)
+  - [结构体](./getting-to-know/structures.md)
+  - [数据类型、模式匹配与递归](./getting-to-know/datatypes-and-patterns.md)
+  - [多态](./getting-to-know/polymorphism.md)
+  - [其他便利的功能](./getting-to-know/conveniences.md)
+  - [总结](./getting-to-know/summary.md)
 - [Hello, World!](./hello-world.md)
-  - [Running a Program](./hello-world/running-a-program.md)
-  - [Step By Step](./hello-world/step-by-step.md)
-  - [Starting a Project](./hello-world/starting-a-project.md)
-  - [Worked Example: `cat`](./hello-world/cat.md)
-  - [Additional Conveniences](./hello-world/conveniences.md)
-  - [Summary](./hello-world/summary.md)
-- [Interlude: Propositions, Proofs, and Indexing](props-proofs-indexing.md)
-- [Overloading and Type Classes](type-classes.md)
-  - [Positive Numbers](type-classes/pos.md)
-  - [Type Classes and Polymorphism](type-classes/polymorphism.md)
-  - [Controlling Instance Search](type-classes/out-params.md)
-  - [Arrays and Indexing](type-classes/indexing.md)
-  - [Standard Classes](type-classes/standard-classes.md)
-  - [Coercions](type-classes/coercion.md)
-  - [Additional Conveniences](type-classes/conveniences.md)
-  - [Summary](type-classes/summary.md)
-- [Monads](./monads.md)
-  - [The Monad Type Class](./monads/class.md)
-  - [Example: Arithmetic in Monads](./monads/arithmetic.md)
-  - [`do`-Notation for Monads](./monads/do.md)
-  - [The `IO` Monad](./monads/io.md)
-  - [Additional Conveniences](monads/conveniences.md)
-  - [Summary](monads/summary.md)
-- [Functors, Applicative Functors, and Monads](functor-applicative-monad.md)
-  - [Structures and Inheritance](functor-applicative-monad/inheritance.md)
-  - [Applicative Functors](functor-applicative-monad/applicative.md)
-  - [The Applicative Contract](functor-applicative-monad/applicative-contract.md)
-  - [Alternatives](functor-applicative-monad/alternative.md)
-  - [Universes](functor-applicative-monad/universes.md)
-  - [The Complete Definitions](functor-applicative-monad/complete.md)
-  - [Summary](functor-applicative-monad/summary.md)
-- [Monad Transformers](monad-transformers.md)
-  - [Combining IO and Reader](monad-transformers/reader-io.md)
-  - [A Monad Construction Kit](monad-transformers/transformers.md)
-  - [Ordering Monad Transformers](monad-transformers/order.md)
-  - [More `do` Features](monad-transformers/do.md)
-  - [Additional Conveniences](monad-transformers/conveniences.md)
-  - [Summary](monad-transformers/summary.md)
-- [Programming with Dependent Types](dependent-types.md)
-  - [Indexed Families](dependent-types/indexed-families.md)
-  - [The Universe Design Pattern](dependent-types/universe-pattern.md)
-  - [Worked Example: Typed Queries](dependent-types/typed-queries.md)
-  - [Indices, Parameters, and Universe Levels](dependent-types/indices-parameters-universes.md)
-  - [Pitfalls of Programming with Dependent Types](dependent-types/pitfalls.md)
-  - [Summary](./dependent-types/summary.md)
-- [Interlude: Tactics, Induction, and Proofs](./tactics-induction-proofs.md)
-- [Programming, Proving, and Performance](programs-proofs.md)
-  - [Tail Recursion](programs-proofs/tail-recursion.md)
-  - [Proving Equivalence](programs-proofs/tail-recursion-proofs.md)
-  - [Arrays and Termination](programs-proofs/arrays-termination.md)
-  - [More Inequalities](programs-proofs/inequalities.md)
-  - [Safe Array Indices](programs-proofs/fin.md)
-  - [Insertion Sort and Array Mutation](programs-proofs/insertion-sort.md)
-  - [Special Types](programs-proofs/special-types.md)
-  - [Summary](programs-proofs/summary.md)
+  - [运行](./hello-world/running-a-program.md)
+  - [逐步运行](./hello-world/step-by-step.md)
+  - [启动项目](./hello-world/starting-a-project.md)
+  - [现实示例：`cat`](./hello-world/cat.md)
+  - [其他便利的功能](./hello-world/conveniences.md)
+  - [总结](./hello-world/summary.md)
+- [插曲：命题、证明与索引](props-proofs-indexing.md)
+- [重载与类型类](type-classes.md)
+  - [正数](type-classes/pos.md)
+  - [类型类与多态](type-classes/polymorphism.md)
+  - [控制实例搜索](type-classes/out-params.md)
+  - [数组与索引](type-classes/indexing.md)
+  - [标准类](type-classes/standard-classes.md)
+  - [强制转换](type-classes/coercion.md)
+  - [其他便利的功能](type-classes/conveniences.md)
+  - [总结](type-classes/summary.md)
+- [单子](./monads.md)
+  - [单子类型类](./monads/class.md)
+  - [示例：用单子表达算术运算](./monads/arithmetic.md)
+  - [单子的 `do`-记法](./monads/do.md)
+  - [`IO` 单子](./monads/io.md)
+  - [其他便利的功能](monads/conveniences.md)
+  - [总结](monads/summary.md)
+- [函子、应用函子与单子](functor-applicative-monad.md)
+  - [结构和继承](functor-applicative-monad/inheritance.md)
+  - [应用函子](functor-applicative-monad/applicative.md)
+  - [应用函子的法则](functor-applicative-monad/applicative-contract.md)
+  - [选择子](functor-applicative-monad/alternative.md)
+  - [全类](functor-applicative-monad/universes.md)
+  - [完整定义](functor-applicative-monad/complete.md)
+  - [总结](functor-applicative-monad/summary.md)
+- [单子变换器](monad-transformers.md)
+  - [组合 IO 与 Reader](monad-transformers/reader-io.md)
+  - [单子构建工具包](monad-transformers/transformers.md)
+  - [对单子变换器排序](monad-transformers/order.md)
+  - [更多 `do` 的特性](monad-transformers/do.md)
+  - [其他便利的功能](monad-transformers/conveniences.md)
+  - [总结](monad-transformers/summary.md)
+- [依值类型编程](dependent-types.md)
+  - [索引族](dependent-types/indexed-families.md)
+  - [全类设计模式](dependent-types/universe-pattern.md)
+  - [现实示例：类型化查询](dependent-types/typed-queries.md)
+  - [索引、形参与全类层级](dependent-types/indices-parameters-universes.md)
+  - [依值类型编程的陷阱](dependent-types/pitfalls.md)
+  - [总结](./dependent-types/summary.md)
+- [插曲：策略、归纳与证明](./tactics-induction-proofs.md)
+- [编程、证明与性能](programs-proofs.md)
+  - [尾递归](programs-proofs/tail-recursion.md)
+  - [证明等价](programs-proofs/tail-recursion-proofs.md)
+  - [数组与停机](programs-proofs/arrays-termination.md)
+  - [更多不等式](programs-proofs/inequalities.md)
+  - [安全数组索引](programs-proofs/fin.md)
+  - [插入排序与数组可变性](programs-proofs/insertion-sort.md)
+  - [特殊类型](programs-proofs/special-types.md)
+  - [总结](programs-proofs/summary.md)
 
-[Next Steps](next-steps.md)
+[接下来做什么](next-steps.md)