MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "MeasuresTypo.ma" ---
--- scope checking ---
--- type checking ---
type  Bool : Set
term  Bool.true : < Bool.true : Bool >
term  Bool.false : < Bool.false : Bool >
type  N : Set
term  N.zz : < N.zz : N >
term  N.ss : ^(y0 : N) -> < N.ss y0 : N >
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  even : .[i : Size] -> Nat i -> Bool
term  even' : .[i : Size] -> Nat i -> Bool
term  odd' : .[i : Size] -> Nat i -> Bool
error during typechecking:
even'
/// clause 2
/// right hand side
/// checkExpr 3 |- odd' i n : Bool
/// inferExpr' odd' i n
/// checkGuard |i,0| < |i,0|
/// lexSizes: no descent detected