chore: add more preludes

web/components/LambdaPlayground.vue

@@ -5,7 +5,7 @@ import LambdaInteractive from './LambdaInteractive.vue';
 import { ref } from 'vue';
 import { useDebounceFn } from '@vueuse/core'
 
-const inputContent = ref('Y I')
+const inputContent = ref('Y Fact (\\f. \\x. f x)')
 const expStr = ref(inputContent.value)
 
 const initWithStr = useDebounceFn((s: string) => {

web/components/playground.lambda

@@ -4,8 +4,12 @@ T = \x. \y. x
 F = \x. \y. y
 O = \f. \x. x
 S = \n. \f. \x. f (n f x)
+P = \n. \f. \x. n (\g. \h. h (g f)) (\u. x) (\u. u)
 One = \f. \x. f x
 Two = \f. \x. f (f x)
 Plus = \n. \m. \f. \x. n f (m f x)
 Mul = \n. \m. \f. \x. n (m f) x
-Exp = \n. \m. n (Mul m) One
+Exp = \n. \m. n (Mul m) One
+IfThenElse = \e. \x. \y. e x y
+IsZero = \n. n (\x. F) T
+Fact = \f. \n. (IsZero n) One (Mul n (f (P n)))

web/docs/ch01-intro.md

@@ -11,8 +11,6 @@ Lambda (`/ˈlæmdə/`，大写形式 Λ, 小写形式 **λ**) 是希腊字母表
 
 称 {L} 道生万物，因为它拥有最简洁的符号定义，却足以构建起一个可靠的逻辑系统，似一门晦涩难懂的语言。可若说它只能被相关专业领域的人所理解，那也有失偏颇。我希望在阅读本文的过程中，每位读者都能够感受到 {L} 的优美和浪漫。但愿以我匮乏的文字表述，能够勉强揭开它潜藏的奥妙。
 
-准备好开始这次的思维之旅了么？
-
 ::: info 声明
 
 本站对 {L} 的叙述主要面向对相关领域（高阶函数、函数式编程、形式验证与自动证明、代数类型系统）不了解的同学，因此很多地方的叙述不够严谨，希望大家多多海涵。也欢迎大家对不妥的部分提出修改意见！

web/docs/ch03-redex.md

@@ -123,4 +123,4 @@ f z
 
 ## 结束也是开始
 
-我想，演算的部分已经告一段落，但我们所见识的 {L} 仍只是冰山一角。请大家放心，梦还很长。函数何为第一要义？道生万物于何处？从下一章开始，从 {l} 与自然数的关系出发，我们再来细说（希望不会颠覆你的认知 :）。准备好了吗？
+我想，演算的部分已经告一段落，但我们所见识的 {L} 仍只是冰山一角。请大家放心，梦还很长。函数何为第一要义？道生万物于何处？从下一章开始，从 {l} 与自然数的关系出发，我们再来细说。

web/docs/index.md

@@ -5,7 +5,7 @@ title: 首页
 hero:
   name: 'λ-Calculus: 道生万物'
   text: 函数抽象的演绎之理
-  tagline: 即使你并不懂计算机！
+  tagline: 现在看来这个标题属实有点中二了 >_<
   actions:
     - theme: brand
       text: 开始阅读

web/docs/playground.md

@@ -16,6 +16,7 @@ import { data } from '../components/playground.data'
 <LambdaDefs :file="data" />
 
 尝试在下方输入框中写一些 Lambda 表达式。点击下划线部分可以化简表达式，可以使用预定义的表达式，点击预定义表达式的别名可以将其展开。
+可以猜猜看这个表达式在计算什么～
 
 <ClientOnly>
   <LambdaPlayground />