4 ms·
Pierre 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 diffe
by Jweb_Guru 5y ago
Pierre 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.