MiniAgda-0.2022.3.11: test/succeed/MeasureInFunTele.ma
-- 2012-02-22
cofun T : -(i : Size)|i| -> Set
{ T i = [j < i] -> T j
}
fun bla : [i : Size] |i| -> T i
{ bla i = bla
}
-- should succeed
-- 2012-02-22
cofun T : -(i : Size)|i| -> Set
{ T i = [j < i] -> T j
}
fun bla : [i : Size] |i| -> T i
{ bla i = bla
}
-- should succeed