how can i read a vec filter?

If you look at the definition of Vec≤, you will see that it is already exactly what you are asking for:

record Vec≤ (A : Set a) (n : ℕ) : Set a where
  constructor _,_
  field {length} : ℕ
        vec      : Vec A length
        .bound   : length ≤ n

So vec of a Vec≤ A n is a “normal” Vec A length, for some length less than n.

CLICK HERE to find out more related problems solutions.

Leave a Comment

Your email address will not be published.

Scroll to Top