在Agda中，可以使用递归函数来过滤掉Vec中的元素。下面是一个示例代码：

open import Data.Vec

filterVec : {A : Set} → (A → Bool) → {n : ℕ} → Vec A n → Vec A _
filterVec p [] = []
filterVec p (x ∷ xs) with p x
... | true = x ∷ filterVec p xs
... | false = filterVec p xs

在上面的代码中，filterVec是一个递归函数，用于过滤掉Vec中的元素。它接受一个谓词函数p，将其应用于Vec中的每个元素。如果谓词函数返回true，则将该元素加入到结果Vec中；否则，将其忽略。递归的基本情况是Vec为空，此时返回一个空的Vec。递归的步骤是将首个元素应用于谓词函数，根据结果决定是否将其加入到结果Vec中，并递归地处理剩余的Vec。

以下是一个使用示例：

filterEven : {n : ℕ} → Vec ℕ n → Vec ℕ _
filterEven = filterVec (λ x → x % 2 ≡ 0)

example : filterEven (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ≡ 2 ∷ 4 ∷ []
example = refl

在上面的代码中，我们定义了一个谓词函数filterEven，用于过滤掉Vec中的奇数。我们将它应用于一个包含1、2、3、4的Vec，并验证过滤结果是否为包含2和4的Vec。