miscelleaneous

Random Lean experiments

  1. 1
def a:=["def a:=","def main:=IO.println s!\"{a[0]}[\\\"{a[0]}\\\",\\\"{a[1].replace \"\\\\\" \"\\\\\\\\\"|>.replace \"\\\"\" \"\\\\\\\"\"}\\\"]{a[1]}\""]def main:=IO.println s!"{a[0]}[\"{a[0]}\",\"{a[1].replace "\\" "\\\\"|>.replace "\"" "\\\""}\"]{a[1]}"