|
|
|
|
|
|
by danilafe
48 days ago
|
|
|
To be fair, Coq has ProofGeneral and Agda has its emacs mode. Once you go outside these established channels, oftentimes using the tool becomes incredibly difficult. I guess for interactive theorem proving in general you may need some sort of editor at some point. |
|
|