File tree Expand file tree Collapse file tree 1 file changed +9
-6
lines changed Expand file tree Collapse file tree 1 file changed +9
-6
lines changed Original file line number Diff line number Diff line change @@ -38,17 +38,19 @@ reduce Intersect{Type x}:
38
38
reduce Intersect{Not(Any), Type... xs}:
39
39
=> Not(Any)
40
40
41
- reduce Intersect{Any, Type... xs}:
42
- => Intersect (xs), if |xs| > 0
41
+ reduce Intersect{Any, Type... xs}
42
+ requires |xs| > 0:
43
+ => Intersect (xs)
43
44
44
45
reduce Intersect{Int, Pair y, Type... ys}:
45
46
=> Not(Any)
46
47
47
48
reduce Intersect{Intersect{Type... xs}, Type... ys}:
48
49
=> Intersect (xs ++ ys)
49
50
50
- reduce Intersect{Not(Type x), Type y, Type... ys}:
51
- => Not(Any), if x == y
51
+ reduce Intersect{Not(Type x), Type y, Type... ys}
52
+ requires x == y:
53
+ => Not(Any)
52
54
53
55
reduce Intersect{Union{Type... xs}, Type... ys}:
54
56
=> let ys = { Intersect(x ++ ys) | x in xs }
@@ -76,8 +78,9 @@ reduce Union{Not(Any), Type... xs}:
76
78
=> Union (xs), if |xs| > 0
77
79
=> Not(Any)
78
80
79
- reduce Union{Not(Type x), Type y, Type... ys}:
80
- => Any, if x == y
81
+ reduce Union{Not(Type x), Type y, Type... ys}
82
+ requires x == y:
83
+ => Any
81
84
82
85
reduce Union{Union{Type... xs}, Type... ys}:
83
86
=> Union (xs ++ ys)
You can’t perform that action at this time.
0 commit comments