Fix reg030.
commit7868829be4fb96dea02fa3c9324327f472d191b2
authorMatus Tejiscak <ziman@functor.sk>
dateThu 29 May 2014, 15:44 (12 years ago)
parent42c28d2
test/reg030/reg030.idr+1−1
@@ -8,7 +8,7 @@ isSubsetOf {univ} a b = (c : univ) -> (member c a) -> (member c b)
88
99class Set univ => HasPower univ where
1010 Powerset : (a : univ) ->
11− Pair univ (\Pa => (c : univ) ->
11+ Sigma univ (\Pa => (c : univ) ->
1212 (isSubsetOf c a) -> member c Pa)
1313
1414powerset : HasPower univ => univ -> univ