[Agda] "data Null" for List

[Sergei Meshveliani]

People,

a function  foo  needs an argument stating that a certain list is empty:

  foo : (null primaryItems ≡ true) → Foo 

And this expression with  "≡ true"  looks awkward.

Has it sense to introduce

  data Null {α} {A : Set α} : List A → Set α  where  isNull : Null []  

and then, to write

  foo : Null primaryItems → Foo 
  foo isNull = ...
?

Thanks,

------
Sergei