MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "ExistsSPos.ma" ---
--- scope checking ---
--- type checking ---
type  Exists : ^(A : Set) -> ++(B : A -> Set) -> Set
term  Exists.exI : .[A : Set] -> .[B : A -> Set] -> ^(witness : A) -> ^(proof : B witness) -> < Exists.exI witness proof : Exists A B >
term  witness : .[A : Set] -> .[B : A -> Set] -> (exI : Exists A B) -> A
{ witness [A] [B] (Exists.exI #witness #proof) = #witness
}
term  proof : .[A : Set] -> .[B : A -> Set] -> (exI : Exists A B) -> B (witness [A] [B] exI)
{ proof [A] [B] (Exists.exI #witness #proof) = #proof
}
type  Foo : Set
term  Foo.foo : ^(y0 : Exists Foo (\ x -> Foo)) -> < Foo.foo y0 : Foo >
error during typechecking:
checking positivity
/// polarity check ++ <= ^ failed