From e9399b162bb770d0af6a8a065683d0e4e10ba8a5 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Tue, 4 Apr 2023 13:30:06 +0200
Subject: [PATCH] add quine example

---
 Quine/Main.lean      |  5 +++++
 Quine/README.md      | 20 ++++++++++++++++++++
 Quine/lakefile.lean  | 15 +++++++++++++++
 Quine/lean-toolchain |  1 +
 README.md            |  5 +++++
 5 files changed, 46 insertions(+)
 create mode 100644 Quine/Main.lean
 create mode 100644 Quine/README.md
 create mode 100644 Quine/lakefile.lean
 create mode 100644 Quine/lean-toolchain

diff --git a/Quine/Main.lean b/Quine/Main.lean
new file mode 100644
index 0000000..bd47fc0
--- /dev/null
+++ b/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)
diff --git a/Quine/README.md b/Quine/README.md
new file mode 100644
index 0000000..57b5e10
--- /dev/null
+++ b/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.
diff --git a/Quine/lakefile.lean b/Quine/lakefile.lean
new file mode 100644
index 0000000..9ba9854
--- /dev/null
+++ b/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
+}
diff --git a/Quine/lean-toolchain b/Quine/lean-toolchain
new file mode 100644
index 0000000..6a9c6db
--- /dev/null
+++ b/Quine/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly
diff --git a/README.md b/README.md
index 4230b3c..166fb0b 100644
--- a/README.md
+++ b/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.