numbat
numbat copied to clipboard
`info` command doesn't have custom tab completion
When typing info is_emp<TAB>, it completes to info is_empty(, including the trailing opening parenthesis. More generally, info <TAB> offers the same 856 candidates that <TAB> on an empty line would.
Thank you for reporting this.
It would be nice if we can fix this. There might be some clash between the "language" Numbat (which doesn't know about commands such as info) and the Numbat REPL, but since we implement tab-completion for specific "frontends", this should be fine. Maybe we even have some command-specific command-completion already.