From b09058085ced03d0594192c517f3944b5527d2ad Mon Sep 17 00:00:00 2001
From: qwjyh <urataw421@gmail.com>
Date: Thu, 5 Jun 2025 06:50:49 +0900
Subject: [PATCH] lint

---
 basics/main.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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