mid of basics

basics/main.lean

@@ -0,0 +1,156 @@
+--- Data and Functions
+
+inductive Day : Type :=
+  | Monday
+  | Tuesday
+  | Wednesday
+  | Thursday
+  | Friday
+  | Saturday
+  | Sunday
+deriving Repr
+
+def next_weekday (d : Day) : Day :=
+  match d with
+  | .Monday => .Tuesday
+  | .Tuesday => .Wednesday
+  | .Wednesday => .Thursday
+  | .Thursday => .Friday
+  | .Friday | .Saturday | .Sunday => .Monday
+
+#eval next_weekday Day.Friday
+#eval next_weekday (next_weekday .Saturday)
+
+theorem test_next_weekday : next_weekday (next_weekday .Saturday) = .Tuesday := by
+  rfl
+
+--- Booleans
+#print bool
+#eval not true
+#print not
+#print and
+#print or
+
+example : or true false = true := by rfl
+example : or false false = false := by rfl
+example : or false true = true := by rfl
+example : or true true = true := by rfl
+
+#eval true ∨ false
+example : true ∨ false = true := by
+  simp
+example : false ∨ false ∨ true = true := by
+  simp
+
+def negb' (b : Bool) : Bool :=
+  if b then false
+  else true
+
+#eval negb' true
+example : negb' true = ¬ true := by
+  simp
+  rfl
+
+--- Exercise 1
+namespace Exercise1
+
+def nandb (b₁ : Bool) (b₂ : Bool) : Bool :=
+  match (b₁, b₂) with
+  | (true, true) => false
+  | _            => true
+
+example : (nandb true false) = true := by
+  rfl
+
+example : (nandb false false) = true := by
+  rfl
+
+example : (nandb false true) = true := by
+  rfl
+example : (nandb true true) = false := by
+  rfl
+
+def andb3
+  | true, true, true => true
+  | _, _, _          => false
+
+example : andb3 true true true = true := by rfl
+example : andb3 false true true = false := by rfl
+example : andb3 true false true = false := by rfl
+example : andb3 true true false = false := by rfl
+
+end Exercise1
+
+--- Types
+
+#check true
+#check Bool.not
+#check true.not
+#check not
+
+--- New Types from Old
+
+inductive Rgb : Type :=
+  | red
+  | green
+  | blue
+
+inductive Color : Type :=
+  | black
+  | white
+  | primary (p : Rgb)
+
+#check Color.primary
+
+def monochrome (c : Color) : Bool :=
+  match c with
+  | .black => true
+  | .white => true
+  | .primary _p => false
+
+def isred (c : Color) : Bool :=
+  match c with
+  | .primary .red => true
+  | _ => false
+
+--- Modules
+namespace Playground
+
+def foo : Rgb := .blue
+
+end Playground
+
+def foo : Bool := true
+
+#check Playground.foo
+#check foo
+
+--- Tuples
+namespace TuplePlayground
+
+inductive Bit : Type :=
+  | B₁
+  | B₀
+
+inductive Nybble :=
+  | bits (b₀ b₁ b₂ b₃ : Bit)
+
+#print Nybble
+
+#check Nybble.bits .B₁ .B₀ .B₁ .B₀
+
+def all_zero (nb : Nybble) : Bool :=
+  match nb with
+  | .bits .B₀ .B₀ .B₀ .B₀ => true
+  | .bits _ _ _ _ => false
+
+#eval all_zero (.bits .B₁ .B₁ .B₁ .B₁)
+#eval all_zero (.bits .B₀ .B₀ .B₀ .B₀)
+
+end TuplePlayground
+
+--- Numbers
+namespace NatPlayground
+
+end NatPlayground
+