Condense quines by using a[0] instead of a.head (by decide)

Changes

3 changed files (+10/-10)

• Quine.lean
  • @@ -1,1 +1,1 @@
    - def a:=["def a:=", "def main:=IO.println s!\"{a.head (by decide)}{a.map λx↦s!\"\\\"{x.replace \"\\\\\" \"\\\\\\\\\"|>.replace \"\\\"\" \"\\\\\\\"\"}\\\"\"}{a.tail.head (by decide)}\""]def main:=IO.println s!"{a.head (by decide)}{a.map λx↦s!"\"{x.replace "\\" "\\\\"|>.replace "\"" "\\\""}\""}{a.tail.head (by decide)}" + 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]}"
• QuineEval.lean
  • @@ -1,5 +1,5 @@
    def a := - ["def a :=", "#eval IO.println <| a.head (by decide)\n#eval a\n#eval IO.println <| a.tail.head (by decide)"] - #eval IO.println <| a.head (by decide) + ["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.tail.head (by decide) + #eval IO.println <| a[1]
• QuineLong.lean
  • @@ -1,9 +1,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)"] + IO.println <| a[0] + IO.println <| a.map fun (x : String) ↦ \"\\\"\" ++ (x.replace \"\\\\\" \"\\\\\\\\\" |>.replace \"\\\"\" \"\\\\\\\"\") ++ \"\\\"\" + IO.println <| a[1]"] 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) + IO.println <| a[0] + IO.println <| a.map fun (x : String) ↦ "\"" ++ (x.replace "\\" "\\\\" |>.replace "\"" "\\\"") ++ "\"" + IO.println <| a[1]