λ is considered bad style

Changes

3 changed files (+11/-7)

• CommitGraph.lean
  • @@ -38,7 +38,7 @@ instance : LE PlainDate := leOfOrd
    def main : IO Unit := do let stdin ← IO.getStdin - let lines := (← stdin.readToEnd).splitOn "\n" |>.toArray |>.filterMap λ x ↦ + let lines := (← stdin.readToEnd).splitOn "\n" |>.toArray |>.filterMap fun x ↦ (Timestamp.toPlainDateAssumingUTC ∘ Timestamp.ofSecondsSinceUnixEpoch ∘ Second.Offset.ofNat) <$> x.toNat? let sorted_lines := lines.qsortOrd if h : 0 < sorted_lines.size then
• Plot.lean
  • @@ -2,17 +2,17 @@ import Std.Time
    open Std.Time def parse_csv filename (parse_row : List String → Option α) := do - return (← IO.FS.readFile filename).splitOn "\n" |>.toArray |>.map (λ (l : String) ↦ + return (← IO.FS.readFile filename).splitOn "\n" |>.toArray |>.map (fun (l : String) ↦ l.replace "\\," "\n" |>.splitOn "," - |>.map λ (s : String) ↦ s.replace "\n" ",") + |>.map fun (s : String) ↦ s.replace "\n" ",") |>.filterMap parse_row instance : LT (DateTime TimeZone.UTC) := ltOfOrd instance : LE PlainDate := leOfOrd def main (args : List String) := do - let lines ← parse_csv args[1]! λ l ↦ match l with + let lines ← parse_csv args[1]! fun l ↦ match l with | [a, b, c] => match ZonedDateTime.fromISO8601String b with | .ok b => some (b.toDateTime.convertTimeZone TimeZone.UTC, ZonedDateTime.fromISO8601String c
  • @@ -21,8 +21,8 @@ def main (args : List String) := do
    | _ => none | _ => none -- Must be LT not LE! - let sorted_starts := lines.qsort λ x y ↦ x.1 < y.1 - let sorted_ends := lines.qsort λ x y ↦ x.2 < y.2 + let sorted_starts := lines.qsort (·.1 < ·.1) + let sorted_ends := lines.qsort (·.2 < ·.2) IO.println <| sorted_ends.map Prod.snd let start_date := date("2025-03-01") let mut date := start_date
  • @@ -43,7 +43,7 @@ def main (args : List String) := do
    j := j + 1 cnt := cnt + 1 daily := daily.push cnt - IO.println s!"{date}{List.replicate (log_size / 2) " " |> "".intercalate}|{List.replicate (total / 2 - log_size / 2) " " |> "".intercalate}|" + IO.println s!"{date}{List.replicate (log_size / 3) " " |> "".intercalate}|{List.replicate (total / 3 - log_size / 3) " " |> "".intercalate}|" date := date.addDays 1 let m := daily.toList.max?.getD 0 let colors := [" ", "░", "▒", "▓", "█"]
• lakefile.toml
  • @@ -18,6 +18,10 @@ root = "Main"
    name = "gcd" root = "Gcd" + [[lean_exe]] + name = "plot" + root = "Plot" + [[lean_exe]] name = "commitgraph" root = "CommitGraph"