MiniAgda-0.2014.1.9: test/fail/ExistsSPos.ma
-- 2010-06-11, Nisse
data Exists (A : Set) (+ B : A -> Set) : Set
{ exI : (witness : A) -> (proof : B witness) -> Exists A B
}
data Foo : Set
{ foo : Exists Foo (\ x -> Foo) -> Foo
}
-- 2010-06-11, Nisse
data Exists (A : Set) (+ B : A -> Set) : Set
{ exI : (witness : A) -> (proof : B witness) -> Exists A B
}
data Foo : Set
{ foo : Exists Foo (\ x -> Foo) -> Foo
}