MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "countingMerge.ma" ---
--- scope checking ---
--- type checking ---
type  Bool : Set
term  Bool.true : < Bool.true : Bool >
term  Bool.false : < Bool.false : Bool >
type  Nat : Set
term  Nat.zero : < Nat.zero : Nat >
term  Nat.suc : ^(y0 : Nat) -> < Nat.suc y0 : Nat >
type  List : Set
term  List.nil : < List.nil : List >
term  List.cons : ^(y0 : Nat) -> ^(y1 : List) -> < List.cons y0 y1 : List >
term  leq : Nat -> Nat -> Bool
{}
term  merge : List -> List -> List
term  merge_aux : Nat -> List -> Nat -> List -> Bool -> List
{ merge List.nil l = l
; merge l List.nil = l
; merge (List.cons x xs) (List.cons y ys) = merge_aux x xs y ys (leq x y)
}
{ merge_aux x xs y ys Bool.true = List.cons x (merge xs (List.cons y ys))
; merge_aux x xs y ys Bool.false = List.cons y (merge (List.cons x xs) ys)
}
error during typechecking:
Termination check for mutual block [merge,merge_aux] fails for [merge,merge_aux]