3 commits

Author	SHA1	Message	Date
Jason Yuen	3770b3dcb8	chore: fix spelling errors (#13274) ... This PR fixed typos: ``` 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']*" ```	2026-04-04 07:34:34 +00:00
Wojciech Różowski	7e3e7cf5d9	feat: add cbv annotations to iterators and strings (#12961) ... This PR adds `cbv` annotations to some iterator and string operations. --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>	2026-03-20 11:39:40 +00:00
Wojciech Różowski	54f188160c	fix: cbv handling of ite/dite/decide (#12816) ... This PR solves three distinct issues with the handling of `ite`/`dite`,`decide`. 1) We prevent the simprocs from picking up `noncomputable`, `Classical` instances, such as `Classical.propDecidable`, when simplifying the proposition in `ite`/`dite`/`decide`. 2) We fix a type mismatch occurring when the condition/proposition is unchanged but the `Decidable` instance is simplified. 3) If we rewrite the proposition from `c` to `c'` and the evaluation of the original instance `Decidable c` gets stuck we try fallback path of of obtaining `Decidable c'` instance and evaluating it. This matters when the instance is evaluated via `cbv_eval` lemmas. --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>	2026-03-06 16:18:39 +00:00