1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29

-- https://hirrolot.github.io/posts/why-static-languages-suffer-from-complexity.html

inductive Fmt where
  | Arg : Fmt → Fmt
  | Nat : Fmt → Fmt
  | Char : Char → Fmt → Fmt
  | End

def toFmt : List Char → Fmt
  | '*' :: xs => .Arg <| toFmt xs
  | '#' :: xs => .Nat <| toFmt xs
  | x :: xs => .Char x <| toFmt xs
  | [] => .End

def PrintfType : Fmt → Type 1
  | .Arg fmt => {α : Type} → [ToString α] → α → PrintfType fmt
  | .Nat fmt => Nat → PrintfType fmt
  | .Char _ fmt => PrintfType fmt
  | .End => PLift String

def printf (fmt : String) : PrintfType <| toFmt fmt.toList :=
  let rec printfAux (acc : Array Char) : (fmt : Fmt) → PrintfType fmt
    | .Arg fmt => fun x ↦ printfAux (acc ++ (toString x).toList) fmt
    | .Nat fmt => fun x ↦ printfAux (acc ++ (toString x).toList) fmt
    | .Char c fmt => printfAux (acc.push c) fmt
    | .End => .up <| .ofList acc.toList
  printfAux #[] <| toFmt fmt.toList

#eval printf "Hello * # * *" (-1) 1 [42, 69] "Meow" |>.down