MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "incompleteSizePattern2.ma" ---
--- scope checking ---
--- type checking ---
type  Bool : Set
term  Bool.tt : < Bool.tt : Bool >
term  Bool.ff : < Bool.ff : Bool >
term  bad'' : .[Size] -> Bool
error during typechecking:
bad''
/// clause 1
/// pattern $i
/// successor pattern only allowed in cofun