This little toy is the reason why I created agda-mode. It's an interactive and external tactic framework for the Agda programming language.
I have a blog about this crate.
