|
|
| Некто написал, |
Coqовец про lean:
https://github.com/coq/coq/issues/1
"TL;DR: Lean support for quotients is FUD. They break an essential metatheoretical property of CIC. Coq people care for this kind of properties, and prefer extending the theory much more slowly at a cost of reduced expressivity"
https://github.com/coq/coq/issues/1
"TL;DR: Lean support for quotients is FUD. They break an essential metatheoretical property of CIC. Coq people care for this kind of properties, and prefer extending the theory much more slowly at a cost of reduced expressivity"
Добавить комментарий:
