Example indentation fix

leanprover · Jul 17, 2022 · f53b7a5 · f53b7a5
1 parent 0a6ebbe
commit f53b7a5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/examples/Examples/Intro.lean b/examples/Examples/Intro.lean
@@ -1621,7 +1621,7 @@ end expect
 expect info {{{ pointPosWithType }}}
   #eval (⟨1, 2⟩ : Point)
 message
-  "{ x := 1.000000, y := 2.000000 }
+"{ x := 1.000000, y := 2.000000 }
 "
 end expect