Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Because the editor was not saved before inspecting types, frequently Error(0) messages were shown, as the editor content and the idris representation would differ.
- Loading branch information