MiniAgda-0.2022.3.11: test/succeed/absurdPattern.golden
MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "absurdPattern.ma" ---
--- scope checking ---
--- type checking ---
type Empty : Set
term magic : .[A : Set] -> .[x : Empty] -> A
{ magic [A] [()]
}
--- evaluating ---
--- closing "absurdPattern.ma" ---