fix test

leanprover-community · Aug 18, 2023 · 9a539d8 · 9a539d8
1 parent 030af5d
commit 9a539d8
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/test/says.lean b/test/says.lean
@@ -65,10 +65,9 @@ example : True := by
   trivial
 
 set_option says.verify true in
-example : Nat := by
-  simp? says simp only
+example (x y : List α) : (x ++ y).length = x.length + y.length := by
+  simp? says simp only [List.length_append]
   -- This is a comment to test that `says` ignores following comments.
-  exact 0
 
 set_option says.no_verify_in_CI true in
 example : True := by