MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "HOMatching.ma" ---
--- scope checking ---
--- type checking ---
type  Succ : Set
term  Succ.succ : ^(y0 : Succ) -> < Succ.succ y0 : Succ >
type  homatch : (Succ -> Succ) -> Set
error during typechecking:
homatch
/// clause 1
/// pattern succ
/// cannot resolve constructor succ