Skip to content

Commit edfaa1a

Browse files
committed
Revised lean with its variables.
1 parent 7bd2fe7 commit edfaa1a

File tree

1 file changed

+4
-4
lines changed

1 file changed

+4
-4
lines changed

lean/ClockHands.lean

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
def printTimes : List (IO Unit) → IO Unit
22
| [] => pure ()
3-
| act :: actions => do
4-
printTimes actions
5-
act
3+
| doPrint :: printStatements => do
4+
printTimes printStatements
5+
doPrint
66

77
def pad : Nat → String
88
| n + 10 => s!"{n + 10}"
@@ -13,6 +13,6 @@ def clock (t : Nat) : String :=
1313

1414
def countdown : Nat → List (IO Unit)
1515
| 0 => []
16-
| n + 1 => IO.println (clock ((43200 * (n) + 21600) / 11)) :: countdown n
16+
| i + 1 => IO.println (clock ((43200 * i + 21600) / 11)) :: countdown i
1717

1818
def main : IO Unit := printTimes (countdown 11)

0 commit comments

Comments
 (0)