Holes (goals) are not numbered #172
Description
There are two cases. Consider this example:
module Test where
open import Data.Bool
f : Bool -> Bool
f = ?When I do a load with :CornelisLoad, the info area displays:
Visible Goals:
?0 : Bool -> Bool
While there is no change to the program (i.e., ? still remains the same and is not substituted). Using Emacs and the agda-mode, a load will change the program to:
f : Bool -> Bool
f = { }0With the info area displaying ?0 : Bool -> Bool, which (the ?0) matches the hole in the program and gives clearer context. This also happens when you do a case split :CornelisMakeCase on ?, which is then substituted with {! !}, but with the info area displaying ?0.
Another case:
f : Bool -> Bool
f x = {! !}When I do :CornelisMakeCase on x with the cursor inside {! !}, the program is replaced as:
f : Bool -> Bool
f false = {! !}
f true = {! !}And the info area displays:
Visible Goals:
?0 : Bool
?1 : Bool
Compared with emacs with agda-mode, the program is rewritten as:
f : Bool -> Bool
f false = { }0
f true = { }1So the holes are numbered and match the info area display. This is more important when there are several holes in the program and it lets you see more clearly which info item refers to which hole in the program.
Would it be possible to change the behavior to match that of Emacs/Agda-mode?
I am using Agda 2.7.0.1, Cornelis v2.7.0, and Neovim v0.11.0 on Mac OS 15.3.2. But I believe this is a universal problem.
Thanks!