search

ashinkarov / nvim-agda

Agda interaction pluging for neovim
36 stars 5 forks source link

Support Cmd_solveOne #2

Closed isovector closed 2 years ago

isovector commented 2 years ago

nvim-agda is great! However sometimes when doing equational reasoning, I'd like to get it to fill in the current state of the equality. In emacs I'd call agda2-solveOne, but this functionality doesn't appear to be implemented in nvim-agda.

isovector commented 2 years ago

Looks like this is blocked upstream https://github.com/agda/agda/issues/5751