MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "HungryEtaRecord.ma" ---
--- scope checking ---
--- type checking ---
type  Hungry : -(i : Size) -> Set
term  Hungry.inn : .[i : Size] -> ^(out : .[j < i] -> Hungry j) -> < Hungry.inn out : Hungry i >
term  out : .[i : Size] -> (inn : Hungry i) -> .[j < i] -> Hungry j
{ out [i] (Hungry.inn #out) = #out
}
type  D : .[i : Size] -> Hungry i -> Set
{}
error during typechecking:
unique
/// new i <= #
/// new x : (Hungry v0)
/// new y : (Hungry v0)
/// new d : (D v0 (v1 Up (Hungry v0)))
/// checkExpr 4 |- d : D i y
/// leqVal' (subtyping)  < d : D i x >  <=+  D i y
/// leqVal' (subtyping)  D i x  <=+  D i y
/// leqVal'  x : Hungry i  <=*  y : Hungry i
/// leqVal'  x : Hungry i  <=*  y : Hungry i
/// leqApp: head mismatch x != y