fix the test

leanprover · Aug 5, 2024 · e4f6939 · e4f6939
1 parent bb66d4d
commit e4f6939
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/tests/lean/run/4768.lean b/tests/lean/run/4768.lean
@@ -1,3 +1,4 @@
-example : True := by
-  refine' trivial ..
-  . trivial
+example : True ∧ True := by
+  constructor
+  refine trivial ..
+  . trivial -- this has to be . not · for this test to be useful