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