close goal in example

leanprover · Nov 4, 2023 · 616f717 · 616f717
1 parent 3b88e16
commit 616f717
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
@@ -106,6 +106,7 @@ example : let n := 1; let k := 2; n + k = 3 := by
   /- n✝ : Nat := 1
      k✝ : Nat := 2
      ⊢ n✝ + k✝ = 3 -/
+  rfl
 ```
 -/
 syntax (name := intros) "intros" (ppSpace colGt (ident <|> hole))* : tactic