Skip to content

Commit 797bfec

Browse files
committed
Basics.lean: (misc) Use d0 d1 d2 d3 instead of b0 b1 b2 b3
1 parent a94abe8 commit 797bfec

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

SoftwareFoundationsVol1/Basics.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -183,7 +183,7 @@ namespace TuplePlayground
183183
| b1
184184
| b0
185185
inductive Nybble : Type where
186-
| bits (b0 b1 b2 b3 : Bit)
186+
| bits (d0 d1 d2 d3 : Bit)
187187

188188
#check (Nybble.bits .b1 .b0 .b1 .b0 : Nybble)
189189

0 commit comments

Comments
 (0)