MiniAgda-0.2022.3.11: test/fail/MeasureInValue.ma
-- 2010-07-17
-- measures can only appear in fun-decls
-- caught by the scope-checker
fun f : (i,j : Size) -> |i| -> Set 1
{ f i j = |i| -> Set
}
-- 2010-07-17
-- measures can only appear in fun-decls
-- caught by the scope-checker
fun f : (i,j : Size) -> |i| -> Set 1
{ f i j = |i| -> Set
}