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.head (by decide)
  IO.println <| a.map λ (x : String) ↦ \"\\\"\" ++ (x.replace \"\\\\\" \"\\\\\\\\\" |>.replace \"\\\"\" \"\\\\\\\"\") ++ \"\\\"\"
  IO.println <| a.tail.head (by decide)"]
def main := do
  IO.println <| a.head (by decide)
  IO.println <| a.map λ (x : String)  "\"" ++ (x.replace "\\" "\\\\" |>.replace "\"" "\\\"") ++ "\""
  IO.println <| a.tail.head (by decide)