MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "D1.ma" ---
--- scope checking ---
--- type checking ---
type  D : Set
term  D.abs : ^(y0 : ^ D -> D) -> < D.abs y0 : D >
warning: ignoring error: polarity check ++ <= - failed
warning: ignoring error: polarity check ++ <= + failed
term  app : ^ D -> ^ D -> D
error during typechecking:
app
/// clause 1
/// pattern abs f
/// cannot match pattern abs f against non-computational argument