lean4-htt/tests/lean/traceStateBacktracking.lean
Jason Yuen facc356a0a
chore: fix spelling errors (#10042)
Typos were found with
```
pip install codespell --upgrade
codespell --summary --ignore-words-list enew,forin,fro,happend,hge,ihs,iterm,spred --skip stage0 --check-filenames
codespell --summary --ignore-words-list enew,forin,fro,happend,hge,ihs,iterm,spred --skip stage0 --check-filenames --regex '[A-Z][a-z]*'
codespell --summary --ignore-words-list enew,forin,fro,happend,hge,ihs,iterm,spred --skip stage0 --check-filenames --regex "\b[a-z']*"
```
2025-08-22 07:23:12 +00:00

5 lines
166 B
Text

example (h : 0 = 1) : False := by
first | trace_state; fail | contradiction
example (h : 0 = 1) : False := by
first | trace "first branch"; fail | contradiction