Fix dependent pair names in reg030.
commit5c9ffda0263592f858ec08593bfeb07c135c778a
authorMatus Tejiscak <ziman@functor.sk>
dateThu 22 May 2014, 18:45 (12 years ago)
parent77ea792
libs/prelude/Builtins.idr+1−1
@@ -47,7 +47,7 @@ data LazyType = LazyCodata | LazyEval
4747data Lazy' : LazyType -> Type -> Type where
4848 ||| A delayed computation.
4949 |||
50− |||Delay is inserted automatically by the elaborator where necessary.
50+ ||| Delay is inserted automatically by the elaborator where necessary.
5151 |||
5252 ||| Note that compiled code gives `Delay` special semantics.
5353 ||| @ t whether this is laziness from codata or normal lazy evaluation
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− Exists univ (\Pa => (c : univ) ->
11+ Pair univ (\Pa => (c : univ) ->
1212 (isSubsetOf c a) -> member c Pa)
1313
1414powerset : HasPower univ => univ -> univ