MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "countingBT.ma" ---
--- scope checking ---
--- type checking ---
type  BT : Set
term  BT.lf : < BT.lf : BT >
term  BT.node : ^(y0 : BT) -> ^(y1 : BT) -> < BT.node y0 y1 : BT >
term  f : BT -> BT
term  g : BT -> BT -> BT
{ f (BT.node l (BT.node rl rr)) = g l rr
}
{ g t u = f (BT.node t u)
}
error during typechecking:
Termination check for mutual block [f,g] fails for [f,g]