Skip to content
Snippets Groups Projects

Add notation `wn` of weakly normalizing terms; and prove some common theorems about it.

Merged Robbert Krebbers requested to merge robbert/wn into master
All threads resolved!

Most important common theorem: strongly normalizing → weakly normalizing.

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Ralf Jung
  • added 1 commit

    • fe933ec7 - Apply suggestion to theories/relations.v

    Compare with previous version

  • Robbert Krebbers added 8 commits

    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`.

    Compare with previous version

  • Ralf Jung resolved all threads

    resolved all threads

  • LGTM!

  • Robbert Krebbers resolved all threads

    resolved all threads

  • mentioned in commit b4ec8641

  • Merged, and thanks for the feedback!

  • Please register or sign in to reply
    Loading