|
|
|
|
|
|
by danilafe
51 days ago
|
|
|
Also true. The slowness is relatively unpredictable, too: sometimes changing a 'rewrite' to a 'with' can increase memory usage tenfold. While we're at it, another major concern for me is the inscrutability of Agda's error messages. I've had one error message single-handedly overflow my tmux scrollback buffer. There's no way I'm going to be able to interpret that. |
|
|
lmao i've been there. Agda is my first choice for proof checker and for math-y explorations but its not gonna be a replacement for Haskell as a production programming language.