Skip to content

Commit

Permalink
Update templates/extras/tactic_writing.md
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser authored and PatrickMassot committed Apr 8, 2021
1 parent 76815d2 commit dcd71a6
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion templates/extras/tactic_writing.md
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,7 @@ do `(%%l = %%r) ← tactic.target | tactic.trace "Goal is not an equality",
```

If the `|` is ommitted, then the tactic fails if the pattern does not match.
We can catch this failure using the `orelse` combinator mentioned ealier, but not that by
We can catch this failure using the `orelse` combinator mentioned ealier, but note that by
doing so we catch more types of failure than we did above:
```lean
meta def trace_goal_is_eq : tactic unit :=
Expand Down

0 comments on commit dcd71a6

Please sign in to comment.