Random Lean experiments
def a := ["def a :=", "#eval IO.println <| a.head (by decide)\n#eval a\n#eval IO.println <| a.tail.head (by decide)"] #eval IO.println <| a.head (by decide) #eval a #eval IO.println <| a.tail.head (by decide)