def a:=["def a:=", "def main:=IO.println s!\"{a[0]}{(s!\"\\\"{·.replace \"\\\\\" \"\\\\\\\\\"|>.replace \"\\\"\" \"\\\\\\\"\"}\\\"\")<$>a}{a[1]}\""]def main:=IO.println s!"{a[0]}{(s!"\"{·.replace "\\" "\\\\"|>.replace "\"" "\\\""}\"")<$>a}{a[1]}"
Random Lean experiments
def a:=["def a:=", "def main:=IO.println s!\"{a[0]}{(s!\"\\\"{·.replace \"\\\\\" \"\\\\\\\\\"|>.replace \"\\\"\" \"\\\\\\\"\"}\\\"\")<$>a}{a[1]}\""]def main:=IO.println s!"{a[0]}{(s!"\"{·.replace "\\" "\\\\"|>.replace "\"" "\\\""}\"")<$>a}{a[1]}"