max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix doc

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-16 10:32:00 -07:00
parent 04b7924154
commit fe66523e43
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/tour.md
View file

@ -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`
```