File tree Expand file tree Collapse file tree 3 files changed +3
-3
lines changed Expand file tree Collapse file tree 3 files changed +3
-3
lines changed Original file line number Diff line number Diff line change @@ -80,7 +80,7 @@ in Lean 4 core.
8080* `all_goals convSeq` runs the `conv` tactics on every `conv` goal, collecting all the produced
8181 subgoals (if any).
8282
83- * `any_goals convSeq` is like `all_goals` but succeeds if the tactic sequence succees for any
83+ * `any_goals convSeq` is like `all_goals` but succeeds if the tactic sequence succeeds for any
8484 of the goals.
8585
8686* `case tag => convSeq` focuses on a goal with a given tag, runs the tactic sequence, and then
Original file line number Diff line number Diff line change @@ -118,7 +118,7 @@ example (a b c : ℕ) : a * (b * c) = a * (c * b) := by
118118```
119119
120120In all those cases, only the first match is affected.
121- One can also specify which occurences to convert using an `occs` clause, which
121+ One can also specify which occurrences to convert using an `occs` clause, which
122122creates goals for every matched occurrence. These can then all be handled at once
123123using the `all_goals` combinator.
124124The following performs rewriting only for the second and third occurrences of `b * c`:
Original file line number Diff line number Diff line change @@ -46,7 +46,7 @@ General algebra:
4646 cyclic group : ' IsCyclic'
4747 nilpotent group : ' Group.IsNilpotent'
4848 permutation group of a type : ' Equiv.Perm'
49- structure of fintely generated abelian groups : ' AddCommGroup.equiv_free_prod_directSum_zmod'
49+ structure of finitely generated abelian groups : ' AddCommGroup.equiv_free_prod_directSum_zmod'
5050
5151 Rings :
5252 ring : ' Ring'
You can’t perform that action at this time.
0 commit comments