add quine example

Quine/Main.lean

@@ -0,0 +1,5 @@
+def s := "\ndef main : IO Unit := do\n  IO.println (\"def s := \" ++ s.quote)\n  IO.println (s)"
+
+def main : IO Unit := do
+  IO.println ("def s := " ++ s.quote)
+  IO.println (s)

Quine/README.md

@@ -0,0 +1,20 @@
+## Quine example
+
+This is an example of a program that outputs its own source code.
+
+```bash
+~/lean4-samples/Quine$ lake build && build/bin/quine
+def s := "\ndef main : IO Unit := do\n  IO.println (\"def s := \" ++ s.quote)\n  IO.println (s)"
+
+def main : IO Unit := do
+  IO.println ("def s := " ++ s.quote)
+  IO.println (s)
+~/lean4-samples/Quine$ cat Main.lean
+def s := "\ndef main : IO Unit := do\n  IO.println (\"def s := \" ++ s.quote)\n  IO.println (s)"
+
+def main : IO Unit := do
+  IO.println ("def s := " ++ s.quote)
+  IO.println (s)
+```
+
+This relies on the `quote` method of `String.quote : String → String`, which escapes and quotes a string.

Quine/lakefile.lean

@@ -0,0 +1,15 @@
+import Lake
+open Lake DSL
+
+package quine {
+  -- add package configuration options here
+}
+
+lean_lib Quine {
+  -- add library configuration options here
+}
+
+@[defaultTarget]
+lean_exe quine {
+  root := `Main
+}

Quine/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:nightly

README.md

@@ -56,3 +56,8 @@ in 3D which can be animated with the movement of a slider.
 
 Explore how you can extend the Lean syntax to implement the popular python-style
 [List Comprehension](ListComprehension/README.md).
+
+
+## Quine
+
+A simple [quine](https://en.wikipedia.org/wiki/Quine_(computing)): a program that outputs its own source code.