MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "loopOldNoSizePattern.ma" ---
--- scope checking ---
--- type checking ---
type  SNat : + Size -> Set
term  SNat.zero : .[s!ze : Size] -> .[i < s!ze] -> SNat s!ze
term  SNat.zero : .[i : Size] -> < SNat.zero i : SNat $i >
term  SNat.succ : .[s!ze : Size] -> .[i < s!ze] -> ^ SNat i -> SNat s!ze
term  SNat.succ : .[i : Size] -> ^(y1 : SNat i) -> < SNat.succ i y1 : SNat $i >
type  Maybe : ++(A : Set) -> Set
term  Maybe.nothing : .[A : Set] -> < Maybe.nothing : Maybe A >
term  Maybe.just : .[A : Set] -> ^(y0 : A) -> < Maybe.just y0 : Maybe A >
type  Nat : Set
type  Nat = SNat #
term  shift_case : .[i : Size] -> Maybe (SNat $i) -> Maybe (SNat i)
{ shift_case [i] Maybe.nothing = Maybe.nothing
; shift_case [.i] (Maybe.just (SNat.zero [i])) = Maybe.nothing
; shift_case [.i] (Maybe.just (SNat.succ [i] x)) = Maybe.just x
}
term  shift : .[i : Size] -> (Nat -> Maybe (SNat $i)) -> Nat -> Maybe (SNat i)
term  shift = [\ i ->] \ f -> \ n -> shift_case [i] (f (SNat.succ [#] n))
term  inc : Nat -> Maybe Nat
term  inc = \ n -> Maybe.just (SNat.succ [#] n)
type  Unit : Set
term  Unit.unit : < Unit.unit : Unit >
term  loop : .[i : Size] -> SNat i -> (Nat -> Maybe (SNat i)) -> Unit
term  loop_case : .[i : Size] -> (Nat -> Maybe (SNat i)) -> Maybe (SNat i) -> Unit
error during typechecking:
checking type of loop for admissibility
/// new i : _
/// new f : _
/// new i <= #
/// admType: checking ((SNat v2)::Tm -> {(Nat -> Maybe (SNat i)) -> Unit {i = v2}}) admissible in v2
/// new  : (SNat v2)
/// admType: checking (((SNat #)::Tm -> {Maybe (SNat i) {i = v2}})::Tm -> {Unit {i = v2}}) admissible in v2
/// type  SNat # -> Maybe (SNat i)  not lower semi continuous in  i