The IDE features of slime are quite different to the ones one would want in a theorem prover. In particular many functional languages that aren’t CL have strong

The IDE features of slime are quite different to the ones one would want in a theorem prover. In particular many functional languages that aren’t CL have strong type systems (so you’ll want feedback about the types of things) and poor introspection (so something like swank isn’t so easy). A language like Agda does have good emacs support and can do useful things like help you fill in holes. But every speed bump on the way to setting up a theorem prover is important because the target audience isn’t necessarily programming experts who will go through a lot of pain so long as they can use emacs at the end of it.