MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "huetHullotReverse.ma" ---
--- scope checking ---
--- type checking ---
type  Enum : Set
term  Enum.aa : < Enum.aa : Enum >
term  Enum.bb : < Enum.bb : Enum >
term  Enum.cc : < Enum.cc : Enum >
type  List : ^(A : Set) -> Set
term  List.nil : .[A : Set] -> < List.nil : List A >
term  List.cons : .[A : Set] -> ^(y0 : A) -> ^(y1 : List A) -> < List.cons y0 y1 : List A >
term  list : List Enum
term  list = List.cons Enum.aa (List.cons Enum.bb (List.cons Enum.cc List.nil))
term  rev : .[A : Set] -> List A -> List A
term  rev1 : .[A : Set] -> A -> List A -> A
term  rev2 : .[A : Set] -> A -> List A -> List A
{ rev [A] List.nil = List.nil
; rev [A] (List.cons x xs) = List.cons (rev1 [A] x xs) (rev2 [A] x xs)
}
{ rev1 [A] a List.nil = a
; rev1 [A] a (List.cons x xs) = rev1 [A] x xs
}
{ rev2 [A] a List.nil = List.nil
; rev2 [A] a (List.cons x xs) = rev [A] (List.cons a (rev [A] (rev2 [A] x xs)))
}
error during typechecking:
Termination check for mutual block [rev,rev1,rev2] fails for [rev,rev2]