4 ms·
I haven't used quotients (or Lean), but I've certainly encountered subject reduction problems in Coq when using coinduction, so this sounds a tad hypocritical.
by chriswarbo 5y ago
I haven't used quotients (or Lean), but I've certainly encountered subject reduction problems in Coq when using coinduction, so this sounds a tad hypocritical.
It's certainly good to avoid breaking subject reduction even more though ;)
- xvilka 5y agoThere's ongoing work[1] on fixing that. Also let's see how migrating setoids to cubical type theory might fix more issues for Coq. Will they follow the Arend[2] path? That remains to be seen. [1] https://github.com/coq/coq/pull/10764 https://github.com/coq/coq/pull/10764 [2] https://arend-lang.github.io/about/arend-features https://arend-lang.github.io/about/arend-features
- Jweb_Guru 5y agoPierre Pedrot has been very vocal in his belief that broken SR from coinductive types is a serious problem with Coq that needs to be fixed. This is quite different from introducing stuff that deliberately breaks it.