idris-mode for Emacs does similar tricks ( https://github.com/idris-hackers/idris-mode https://github.com/idris-hackers/idris-mode ) and I've heard it's very ni

idris-mode for Emacs does similar tricks ( https://github.com/idris-hackers/idris-mode https://github.com/idris-hackers/idris-mode ) and I've heard it's very nice. The Idris REPL itself can do hole-based programming too, which can then be dumped out to a file (:m to list holes, :p to prove a hole, :a to write proofs to disk) http://docs.idris-lang.org/en/latest/reference/repl.html http://docs.idris-lang.org/en/latest/reference/repl.html