scratches/software_foundation
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

lint

Browse source
This commit is contained in:
qwjyh 2025-06-05 06:50:49 +09:00
parent 44708b89bf
commit b09058085c
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
basics/main.lean
View file

@ -1,6 +1,6 @@
--- Data and Functions --- Data and Functions
inductive Day : Type := inductive Day : Type where
| Monday | Monday
| Tuesday | Tuesday
| Wednesday | Wednesday
@ -138,11 +138,11 @@ def foo : Bool := true
--- Tuples --- Tuples
namespace TuplePlayground namespace TuplePlayground
inductive Bit : Type := inductive Bit : Type where
| B₁ | B₁
| B₀ | B₀
inductive Nybble := inductive Nybble where
| bits (b₀ b₁ b₂ b₃ : Bit) | bits (b₀ b₁ b₂ b₃ : Bit)
#print Nybble #print Nybble