Add missing file from earlier commit

leanprover · Oct 3, 2023 · 432ffaa · 432ffaa
1 parent af634d3
commit 432ffaa
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/examples/first-lake/expected/Greeting/Basic.lean b/examples/first-lake/expected/Greeting/Basic.lean
@@ -0,0 +1 @@
+def hello := "world"