Like :ps, but instead of a recursive search, it simply applies the
function given and fills in other arguments *by unification only*.
(In particular, this means it will fail if any implicit arguments need
other arguments, rather than the return type, in order to be solved by
unification).
So, this will work:
append : (n, m : Nat) -> Vect n a -> Vect m a -> Vect (n + m) a
append Z m [] ys = ys
append (S k) m (x :: xs) ys = x :: ?append_rhs1
*testref> :ref 6 append_rhs1 append
append k m ?append_rhs2 ?append_rhs3
But this will not:
vZipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
vZipWith f [] [] = []
vZipWith f (x :: xs) (y :: ys) = f x y :: ?vZipWith_rhs1
*Vect> :ref 18 vZipWith_rhs1 vZipWith
?vZipWith_rhs1
...because unification alone is not enough to work out the implicit
arguments a and b (even if there is only one thing that will work, it
needs a deeper proof search to find it).
