0 | module Data.Linear.List.LQuantifiers
 1 |
 2 | import Data.Linear.Notation
 3 |
 4 | %default total
 5 |
 6 | public export
 7 | data LAll : (p : a -> Type) -> List a -> Type where
 8 |   Nil  : LAll p []
 9 |   (::) : p x -@ LAll p xs -@ LAll p (x :: xs)
10 |