Logical Foundations - Basics

steshaw · Jun 28, 2023 · 6bb76c4 · 6bb76c4
1 parent 01360df
commit 6bb76c4
Showing 1 changed file with 27 additions and 0 deletions.
diff --git a/sf-lf/basics.lean b/sf-lf/basics.lean
@@ -0,0 +1,27 @@
+inductive Day : Type :=
+  | monday
+  | tuesday
+  | wednesday
+  | thursday
+  | friday
+  | saturday
+  | sunday
+deriving Repr
+
+def Day.next_weekday (d : Day) : Day :=
+  match d with
+  | monday => tuesday
+  | tuesday => wednesday
+  | wednesday => thursday
+  | thursday => friday
+  | friday => monday
+  | saturday => monday
+  | sunday => monday
+
+#eval Day.friday.next_weekday
+-- Day.monday
+#eval Day.saturday.next_weekday.next_weekday
+-- Day.tuesday
+
+example test_next_weekday: Day.saturday.next_weekday.next_weekday = Day.tuesday :=
+  rfl