MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "BoundedQWrong.ma" ---
--- scope checking ---
--- type checking ---
type  Nat : + Size -> Set
term  Nat.zero : .[s!ze : Size] -> .[i < s!ze] -> Nat s!ze
term  Nat.zero : .[i : Size] -> < Nat.zero i : Nat $i >
term  Nat.succ : .[s!ze : Size] -> .[i < s!ze] -> ^ Nat i -> Nat s!ze
term  Nat.succ : .[i : Size] -> ^(y1 : Nat i) -> < Nat.succ i y1 : Nat $i >
term  mySucc : .[i : Size] -> .[j < i] -> Nat i -> Nat j
block fails as expected, error message:
mySucc
/// clause 1
/// right hand side
/// checkExpr 3 |- succ j n : Nat j
/// checkForced fromList [(j,1),(i,0),(n,2)] |- succ j n : Nat j
/// checkApp (^(y1 : (Nat v1)::()) -> < Nat.succ i y1 : Nat $i >{i = v1}) eliminated by n
/// leqVal' (subtyping)  < n : Nat i >  <=+  Nat j
/// leqVal' (subtyping)  Nat i  <=+  Nat j
/// leqVal'  i  <=+  j : Size
/// leSize i <=+ j
/// leSize' i <= j
/// bound not entailed
error during typechecking:
explicitCast
/// checkExpr 0 |- \ i -> \ j -> \ n -> n : .[i : Size] -> .[j <= i] -> Nat i -> Nat j
/// checkForced fromList [] |- \ i -> \ j -> \ n -> n : .[i : Size] -> .[j <= i] -> Nat i -> Nat j
/// new i <= #
/// checkExpr 1 |- \ j -> \ n -> n : .[j <= i] -> Nat i -> Nat j
/// checkForced fromList [(i,0)] |- \ j -> \ n -> n : .[j <= i] -> Nat i -> Nat j
/// new j <= v0
/// adding size rel. v1 + 0 <= v0
/// checkExpr 2 |- \ n -> n : Nat i -> Nat j
/// checkForced fromList [(j,1),(i,0)] |- \ n -> n : Nat i -> Nat j
/// new n : (Nat v0)
/// checkExpr 3 |- n : Nat j
/// leqVal' (subtyping)  < n : Nat i >  <=+  Nat j
/// leqVal' (subtyping)  Nat i  <=+  Nat j
/// leqVal'  i  <=+  j : Size
/// leSize i <=+ j
/// leSize' i <= j
/// bound not entailed