Hiccup renderer in Lean 4

Hiccup.lean

inductive Hiccup : Type
| tag : String -> List (String × String) -> List Hiccup -> Hiccup
| value : String -> Hiccup
deriving Repr

open Hiccup

partial def render : Hiccup -> String
| tag name attrs rest => s!"<{name} {buildAttrs attrs}>{rest.map render |> String.join}</{name}>"
| value s => s
where
  buildAttrs (kvs : List (String × String)) : String :=
    kvs.map (λ (k, v) => s!"\"{k}\"=\"{v}\"") |> String.intercalate " "

#eval render $ tag "div" [("class", "foo")] [tag "span" [] [value "hello"], value "world"]