Add notation `wn` of weakly normalizing terms; and prove some common theorems about it.
Merged
Add notation `wn` of weakly normalizing terms; and prove some common theorems about it.
robbert/wn
into
master
All threads resolved!
All threads resolved!
Most important common theorem: strongly normalizing → weakly normalizing.
Merge request reports
Activity
Filter activity
- Resolved by Robbert Krebbers
- Resolved by Ralf Jung
added 8 commits
-
fe933ec7...087e4ccf - 5 commits from branch
master
- ff8eccc6 - Add notation `wn` of weakly normalizing terms; and prove some common theorems about it.
- 85fb9ae4 - CHANGELOG.
- 613153f3 - Intuition for decidability of `red` in `wn_sn`.
Toggle commit list-
fe933ec7...087e4ccf - 5 commits from branch
mentioned in commit b4ec8641
Please register or sign in to reply