Y
HN Search
Hacker News Search
new
|
comments
|
top
|
jobs
Zimm_i48
searching PlanetScale…
1.
▲
2.
▲
3.
▲
4.
▲
5.
▲
6.
▲
3 ms
·
1.
▲
by
Zimm_i48
9y ago
You can certainly do readable proofs in Coq the way you would do them in Isabelle, but this requires stating intermediate states explicitly (with assert e.g.) and Coq users rarely do that (mainly because readability is not their goal, I gue
2.
▲
by
Zimm_i48
10y ago
This is because people comment without actually reading the article :/