diff --git a/basics/main.lean b/basics/main.lean
index 900dd14..3496fa4 100755
--- a/basics/main.lean
+++ b/basics/main.lean
@@ -1,6 +1,6 @@
 --- Data and Functions
 
-inductive Day : Type :=
+inductive Day : Type where
   | Monday
   | Tuesday
   | Wednesday
@@ -138,11 +138,11 @@ def foo : Bool := true
 --- Tuples
 namespace TuplePlayground
 
-inductive Bit : Type :=
+inductive Bit : Type where
   | B₁
   | B₀
 
-inductive Nybble :=
+inductive Nybble where
   | bits (b₀ b₁ b₂ b₃ : Bit)
 
 #print Nybble