MiniAgda-0.2014.1.9: test/succeed/omegaInst1.ma

-- 2012-02-06  Make sure not to violate < - Constraints by going through infty
-- (not finished)

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

cofun Bot : +(i : Size) -> Set
{ Bot i = [j < i] & Bot j
}

cofun Top : -(i : Size) -> Set
{ Top i = [j < i] -> Top j
}

fun out : [i : Size] (r :  Top $i) -> Top i
{ out i r j = r $j j }

let inn [i : Size] (t : Top i) : Top $i
  = \ j -> t

let bad [F : Size -> Set] [i <= #] (f : [j < $i] -> F j) : F i
  = f i

fail
let test [F : Size -> Set] = fix F (bad F)