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

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

inductive Fmt where
  | FArg : Fmt → Fmt
  | FChar : Char → Fmt → Fmt
  | FEnd

def toFmt : List Char → Fmt
  | '*' :: xs => .FArg <| toFmt xs
  | x :: xs => .FChar x <| toFmt xs
  | [] => .FEnd

def PrintfType : Fmt → Type 1
  | .FArg fmt => {α : Type} → [ToString α] → α → PrintfType fmt
  | .FChar _ fmt => PrintfType fmt
  | .FEnd => PLift String

def printf (fmt : String) : PrintfType <| toFmt <| fmt.toList :=
  let rec printfAux (fmt : Fmt) (acc : List Char) : PrintfType fmt :=
    match fmt with
    | .FArg fmt => fun x => printfAux fmt <| acc ++ (toString x).toList
    | .FChar c fmt => printfAux fmt <| acc ++ [c]
    | .FEnd => .up acc.asString
  printfAux (toFmt <| fmt.toList) []

#eval printf "Hello * *" 42 "Meow" |>.down