MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "BoundedQ.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 j -> Nat i
{ mySucc [i] [j < i] n = Nat.succ [j] n
}
term  boundedId : .[i : Size] -> .[j <= i] -> (n : Nat j) -> Nat j
term  boundedId = [\ i ->] [\ j ->] \ n -> n
term  explicitCast : .[i : Size] -> .[j <= i] -> Nat j -> Nat i
term  explicitCast = [\ i ->] [\ j ->] \ n -> n
term  explicitCast' : .[i : Size] -> .[j : Size] -> |j| <= |i| -> Nat j -> Nat i
{ explicitCast' [i] [j] n = n
}
--- evaluating ---
--- closing "BoundedQ.ma" ---