MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "negativeFam.ma" ---
--- scope checking ---
--- type checking ---
type  Nat : Set
term  Nat.zero : < Nat.zero : Nat >
term  Nat.suc : ^(y0 : Nat) -> < Nat.suc y0 : Nat >
type  D : ^ Nat -> Set
term  D.abs : ^(y0 : D Nat.zero -> D Nat.zero) -> < D.abs y0 : D Nat.zero >
term  D.app : .[n : Nat] -> ^(y1 : D n) -> ^(y2 : D n) -> < D.app n y1 y2 : D n >
error during typechecking:
checking positivity
/// polarity check ++ <= - failed