miscelleaneous

Random Lean experiments

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
def a :=
["def a :=", "def main := do
  IO.println <| a[0]
  IO.println <| a.map fun (x : String) ↦ \"\\\"\" ++ (x.replace \"\\\\\" \"\\\\\\\\\" |>.replace \"\\\"\" \"\\\\\\\"\") ++ \"\\\"\"
  IO.println <| a[1]"]
def main := do
  IO.println <| a[0]
  IO.println <| a.map fun (x : String)  "\"" ++ (x.replace "\\" "\\\\" |>.replace "\"" "\\\"") ++ "\""
  IO.println <| a[1]