From 5cf5dae9557aa07f0b1baa18ec6ec2da9b841259 Mon Sep 17 00:00:00 2001 From: subfish-zhou Date: Thu, 25 Jul 2024 20:52:19 +0800 Subject: [PATCH] test pr --- lean/main/01_intro.lean | 41 ++++++++++++++++++++++++++--------------- md/SUMMARY.md | 38 +++++++++++++++++++------------------- 2 files changed, 45 insertions(+), 34 deletions(-) diff --git a/lean/main/01_intro.lean b/lean/main/01_intro.lean index 3401465..92a17ef 100644 --- a/lean/main/01_intro.lean +++ b/lean/main/01_intro.lean @@ -1,23 +1,34 @@ /- -# Introduction +-- # Introduction -## What's the goal of this book? +-- ## What's the goal of this book? -This book aims to build up enough knowledge about metaprogramming in Lean 4 so -you can be comfortable enough to: +-- This book aims to build up enough knowledge about metaprogramming in Lean 4 so +-- you can be comfortable enough to: -* Start building your own meta helpers (defining new Lean notation such as `∑`, -building new Lean commands such as `#check`, writing tactics such as `use`, etc.) -* Read and discuss metaprogramming APIs like the ones in Lean 4 core and -Mathlib4 +-- * Start building your own meta helpers (defining new Lean notation such as `∑`, +-- building new Lean commands such as `#check`, writing tactics such as `use`, etc.) +-- * Read and discuss metaprogramming APIs like the ones in Lean 4 core and +-- Mathlib4 -We by no means intend to provide an exhaustive exploration/explanation of the -entire Lean 4 metaprogramming API. We also don't cover the topic of monadic -programming in Lean 4. However, we hope that the examples provided will be -simple enough for the reader to follow and comprehend without a super deep -understanding of monadic programming. The book -[Functional Programming in Lean](https://leanprover.github.io/functional_programming_in_lean/) -is a highly recommended source on that subject. +-- We by no means intend to provide an exhaustive exploration/explanation of the +-- entire Lean 4 metaprogramming API. We also don't cover the topic of monadic +-- programming in Lean 4. However, we hope that the examples provided will be +-- simple enough for the reader to follow and comprehend without a super deep +-- understanding of monadic programming. The book +-- [Functional Programming in Lean](https://leanprover.github.io/functional_programming_in_lean/) +-- is a highly recommended source on that subject. + +# 介绍 + +## 本书的目的 + +本书的目的是在 Lean 4 中建立足够的元编程知识，你将学会： + +- 构建自己的元助手（定义新的 Lean 符号，如「∑」，构建新的 Lean 命令，如`#check`，编写策略，如`use`等） +- 阅读和讨论元编程API，如Lean 4 core和Mathlib4中的API + +我们绝不打算对整个 Lean 4 元编程API进行详尽的解释。我们也不涉及单子（Monad）化编程的主题。我们希望示例足够简单，不太熟悉单子化编程也能跟上。强烈推荐[ Lean 中的函数式编程](https://www.leanprover.cn/fp-lean-zh/)作为这个主题的参考。 ## Book structure diff --git a/md/SUMMARY.md b/md/SUMMARY.md index c6ad0b5..e13f828 100644 --- a/md/SUMMARY.md +++ b/md/SUMMARY.md @@ -1,32 +1,32 @@ -# Summary +# 目录 -# Main +# 正文 -- [Introduction](./main/01_intro.md) -- [Overview](./main/02_overview.md) -- [Expressions](./main/03_expressions.md) +- [介绍](./main/01_intro.md) +- [概述](./main/02_overview.md) +- [表达式](./main/03_expressions.md) - [MetaM](./main/04_metam.md) -- [Syntax](./main/05_syntax.md) -- [Macros](./main/06_macros.md) -- [Elaboration](./main/07_elaboration.md) -- [Embedding DSLs By Elaboration](./main/08_dsls.md) -- [Tactics](./main/09_tactics.md) -- [Lean4 Cheat-sheet](./main/10_cheat-sheet.md) +- [句法](./main/05_syntax.md) +- [宏](./main/06_macros.md) +- [繁饰](./main/07_elaboration.md) +- [通过繁饰嵌入DSL](./main/08_dsls.md) +- [证明策略](./main/09_tactics.md) +- [Lean4速查表](./main/10_cheat-sheet.md) -# Extra +# 额外内容 -- [Options](./extra/01_options.md) +- [选项](./extra/01_options.md) -- [Pretty Printing](./extra/03_pretty-printing.md) +- [美观打印](./extra/03_pretty-printing.md) -# Solutions +# 习题解答 -- [Expressions](./solutions/03_expressions.md) +- [表达式](./solutions/03_expressions.md) - [`MetaM`](./solutions/04_metam.md) -- [`Syntax`](./solutions/05_syntax.md) +- [句法](./solutions/05_syntax.md) -- [Elaboration](./solutions/07_elaboration.md) +- [繁饰](./solutions/07_elaboration.md) -- [Tactics](./solutions/09_tactics.md) +- [证明策略](./solutions/09_tactics.md)