MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "partialFunction.ma" ---
--- scope checking ---
--- type checking ---
type  Subset : ^(A : Set) -> ^(P : A -> Set) -> Set
term  Subset.put : .[A : Set] -> .[P : A -> Set] -> ^(a : A) -> .[y1 : P a] -> < Subset.put a y1 : Subset A P >
type  PFun : ^(A : Set) -> ^(B : Set) -> Set
error during typechecking:
PFun
/// constructor PFun.mkPFun
/// new PFun : (^(A : Set) -> ^(B : Set) -> Set)
/// new A : Set
/// new B : Set
/// inferExpr' ^(dom : A -> Set) -> ^(app : Subset A dom -> B) -> PFun A B
/// new dom : (v1::Tm -> {Set {B = v2, A = v1, PFun = (v0 Up (^(A : Set) -> ^(B : Set) -> Set))}})
/// leSize 1 <=+ 0
/// leSize' 1 <= 0
/// leSize': 1 <= 0 failed