0 | module Network.URL.Internal.Predicate
 1 |
 2 | %default total
 3 |
 4 | --  针对类型a的谓词
 5 | public export
 6 | Predicate : Type -> Type 
 7 | Predicate a = a -> Bool
 8 |
 9 | -- 特别的，如果没有谓词，算是不通过
10 | -- 任意一个通过，算是整体通过
11 | public export
12 | anyPass : List (Predicate a) -> a -> Bool
13 | anyPass [] _ = False
14 | anyPass [p] x = p x
15 | anyPass (p :: ps) x = p x || anyPass ps x
16 |
17 | -- 特别的，如果没有谓词，算是不通过
18 | -- 全部通过，才算是整体通过
19 | public export
20 | allPass : List (Predicate a) -> a -> Bool
21 | allPass [] _ = False
22 | allPass [p] x = p x
23 | allPass (p :: ps) x = p x && allPass ps x
24 |