From fe66523e43f0eb5c6ee4ee4bfe6b2f87d856da75 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 16 Sep 2021 10:32:00 -0700 Subject: [PATCH] chore: fix doc --- doc/tour.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/tour.md b/doc/tour.md index 26c0f36954..f5da909193 100644 --- a/doc/tour.md +++ b/doc/tour.md @@ -196,5 +196,5 @@ theorem Weekday.nextOfPrevious (d : Weekday) : next (previous d) = d := -- using metaprogramming (or "tactics"). theorem Weekday.nextOfPrevious' (d : Weekday) : next (previous d) = d := by cases d -- A proof by case distinction - allGoals rfl -- Each case is solved using `rfl` + all_goals rfl -- Each case is solved using `rfl` ```