packages feed

MiniAgda-0.2014.1.9: test/fail/MixedMeasuredUnmeasured.ma

-- 2010-07-17 

-- mixing measured functions with unmeasured is illegal, 
-- caught by the scope-checker

mutual {
  fun f : (i : Size) -> |i| -> Set {}
  fun g : (i : Size) -> Set {}
}