my_v|ect_map : (a -> b) -> Vect n a -> Vect n b -- ①Generate an initial pattern match clause my_vect_map : (a -> b) -> Vect n a -> Vect n b my_vect_map f x|s = ?my_vect_map_rhs -- ②Generate a case split for a pattern variable my_vect_map : (a -> b) -> Vect n a -> Vect n b my_vect_map f [] = ?my_vect|_map_rhs_1 -- ③Attempt to fill out holes by proof search my_vect_map f (x :: y) = ?my|_vect_map_rhs_2 -- ③Attempt to fill out holes by proof search -- 最終 my_vect_map : (a -> b) -> Vect n a -> Vect n b my_vect_map f [] = [] my_vect_map f (x :: y) = f x :: my_vect_map f y