I don't know Idris so this syntax is probably wrong, but by reading the docs for a short while, this would be
any : (a -> Bool) -> Lazy List a -> Bool
... which would make it as performant and clearer than Haskell's any, since the laziness is explicit.
Someone with actual Idris experience might tell if it actually would work like this :) I guess we'd have to make sure that the used or function is also lazy.