From af18270a018f6ff0d8b2b6bcb947977b9f83c5b8 Mon Sep 17 00:00:00 2001
From: An Ziwu <14214576@cumt.edu.cn>
Date: Tue, 7 Jul 2026 15:33:31 +0800
Subject: [PATCH] basic

---
 RolleTheorem/Basic.lean | 25 ++++++++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)

diff --git a/RolleTheorem/Basic.lean b/RolleTheorem/Basic.lean
index 99415d9..c0dcd45 100644
--- a/RolleTheorem/Basic.lean
+++ b/RolleTheorem/Basic.lean
@@ -1 +1,24 @@
-def hello := "world"
+/- 定义一些常数 -/
+
+def m : Nat := 1       -- m 是自然数
+def n : Nat := 0
+def b1 : Bool := true  -- b1 是布尔型
+def b2 : Bool := false
+
+/- 检查类型 -/
+
+#check m
+#check n
+#check n + 0
+#check m * (n + 0)
+#check b1
+-- "&&" 是布尔与
+#check b1 && b2
+-- 布尔或
+#check b1 || b2
+-- 布尔 "真"
+#check true
+/- 求值（Evaluate） -/
+#eval 5 * 4
+#eval m + 2
+#eval b1 && b2