MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "shouldBeDotPattern_snat.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 >
term  z : SNat #
term  z = SNat.zero [#]
term  one : SNat #
term  one = SNat.succ [#] z
term  two : SNat #
term  two = SNat.succ [#] one
term  three : SNat #
term  three = SNat.succ [#] two
term  add : .[i : Size] -> .[j : Size] -> SNat i -> SNat j -> SNat #
error during typechecking:
add
/// clause 1
/// pattern $i
/// successor pattern only allowed in cofun