MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "match_erased.ma" ---
--- scope checking ---
--- type checking ---
type  Nat : Set
term  Nat.zero : < Nat.zero : Nat >
term  Nat.succ : ^(y0 : Nat) -> < Nat.succ y0 : Nat >
term  illegal_match : Nat -> .[Nat] -> Nat
error during typechecking:
illegal_match
/// clause 1
/// pattern zero
/// checkPattern: constructor Nat.zero of non-computational argument zero : Nat not forced