Merge pull request #3 from subfish-zhou/backup

update tactics&interacting

.gitignore

@@ -3,4 +3,5 @@
 /leanpkg.path
 out/
 .vs/
-.vscode/
+.vscode/
+/src_zh

SUMMARY.md

@@ -1,3 +1,4 @@
+<!--
 # Theorem Proving in Lean 4
 
 [Theorem Proving in Lean 4](title_page.md)
@@ -14,3 +15,22 @@
 - [Type Classes](./type_classes.md)
 - [The Conversion Tactic Mode](./conv.md)
 - [Axioms and Computation](./axioms_and_computation.md)
+
+-->
+
+# Lean 4定理证明
+
+[Lean 4定理证明](title_page.md)
+
+- [介绍](./introduction.md)
+- [依值类型论](./dependent_type_theory.md)
+- [命题和证明](./propositions_and_proofs.md)
+- [量词与等价](./quantifiers_and_equality.md)
+- [证明策略](./tactics.md)
+- [与Lean交互](./interacting_with_lean.md)
+- [归纳类型](./inductive_types.md)
+- [Induction and Recursion](./induction_and_recursion.md)
+- [结构体和记录](./structures_and_records.md)
+- [Type Classes](./type_classes.md)
+- [转换策略模式](./conv.md)
+- [Axioms and Computation](./axioms_and_computation.md)