MiniAgda-0.2022.3.11: test/succeed/Fix.ma

-- 2012-01-27  fix-point principle

fun fix : [A : Size -> Set] ->
  (f : [i : Size] -> ([j < i] -> A j) -> A i) ->
  [i : Size] -> |i| -> A i
{ fix A f i = f i (fix A f)
}