Allow :ps <hole name>

[iacore]

• [ ] I have read CONTRIBUTING.md. The page is missing
• [x] I have checked that there is no existing PR/issue about my proposal.

Summary

I usually use :ps 0 foo to find proof with idris2 REPL. However, It would be nice if :ps foo would show all the search results.

Examples

Given the following file:

data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

%name Vect xs, ys, zs

comp : (a -> b) -> (b -> c) -> a -> c
comp = ?baz

zipWith : (a -> b -> c) -> (1 xs : Vect n a) -> (1 ys : Vect n b) -> Vect n c
zipWith f [] [] = []
zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys

transposeHelper : Vect m a -> (1 xs_trans : Vect m (Vect k a)) -> Vect m (Vect (S k) a)
transposeHelper xs ys = zipWith ?foo xs ys

> idris2 test.idr
     ____    __     _         ___
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.5.1-67951529e
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
 /___/\__,_/_/  /_/____/   /____/      Type :? for help
Welcome to Idris 2.  Enjoy yourself!
Main> :ps foo
(\x, zs => x :: zs)

Technical implementation

Alternatives considered

Conclusion

[iacore]

Also, in the above example, :ps 1 foo is still valid, but returns the same result as :ps 0 foo. Is this a bug?