MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "OverlappingPatternIndFam.ma" ---
--- scope checking ---
--- type checking ---
type  Bool : Set
term  Bool.true : < Bool.true : Bool >
term  Bool.false : < Bool.false : Bool >
type  Id : ^(A : Set) -> ^(a : A) -> ^ A -> Set
term  Id.refl : .[A : Set] -> .[a : A] -> < Id.refl : Id A a a >
term  subst : .[A : Set] -> (a : A) -> (b : A) -> Id A a b -> .[P : A -> Set] -> P a -> P b
{ subst [A] a .a Id.refl [P] x = x
}
type  DecEq : ^(A : Set) -> ^(a : A) -> ^ A -> Set
term  DecEq.eq : .[A : Set] -> .[a : A] -> < DecEq.eq : DecEq A a a >
term  DecEq.notEq : .[A : Set] -> .[a : A] -> .[b : A] -> < DecEq.notEq b : DecEq A a b >
error during typechecking:
offDiag
/// not a type: (A : Set) -> (f : (a : A) -> (b : A) -> DecEq A a b) -> (a : A) -> (b : A) -> Id (DecEq A a b) (f a b) (notEq A a b)
/// inferExpr' (A : Set) -> (f : (a : A) -> (b : A) -> DecEq A a b) -> (a : A) -> (b : A) -> Id (DecEq A a b) (f a b) (notEq A a b)
/// new A : Set
/// inferExpr' (f : (a : A) -> (b : A) -> DecEq A a b) -> (a : A) -> (b : A) -> Id (DecEq A a b) (f a b) (notEq A a b)
/// new f : ((a : v0::Tm) -> (b : A) -> DecEq A a b{A = v0})
/// inferExpr' (a : A) -> (b : A) -> Id (DecEq A a b) (f a b) (notEq A a b)
/// new a : v0
/// inferExpr' (b : A) -> Id (DecEq A a b) (f a b) (notEq A a b)
/// new b : v0
/// inferExpr' Id (DecEq A a b) (f a b) (notEq A a b)
/// checkApp (^(DecEq v0 v2 v3)::Tm -> {Set {a = (v1 v2 v3), A = (DecEq v0 v2 v3)}}) eliminated by notEq A a b
/// checkExpr 4 |- notEq A a b : DecEq A a b
/// checkForced fromList [(A,0),(f,1),(a,2),(b,3)] |- notEq A a b : DecEq A a b
/// checkApp (.[b : v0::Tm] -> < DecEq.notEq b : DecEq A a b >{a = v2, A = v0}) eliminated by A
/// leqVal' (subtyping)  < A : Set >  <=+  A
/// leqVal' (subtyping)  Set  <=+  A
/// leqApp: head mismatch Set != A