miscelleaneous

Random Lean experiments

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
def a :=
["def a :=", "#eval IO.println <| a[0]\n#eval a\n#eval IO.println <| a[1]"]
#eval IO.println <| a[0]
#eval a
#eval IO.println <| a[1]