module Fix

-- from piforall Fix.pi
Type: U
Type = U

-- TODO piforall makes the A in scope for the constructors
-- and has it on the let of the :
-- I think we want that for parameters?
data D : (A : Type) -> Type where
  F : {A : Type} -> (D A -> D A) -> D A
  V : {A : Type} -> A -> D A


-- Here we have two A in play, so y is type of the
-- A in V and the expected return value is the other.
-- We do need to sort this out

unV : { A : U} -> D A -> A
unV (V y) = y
unV (F f) = ?  -- was TRUSTME



-- And here we have D A:4 and D A:1
unF : {A : Type} -> D A -> D A -> D A
unF = \ {A} v x =>
  case v of
    F f => f x
    V y => ? -- was TRUSTME

-- fix : {A : U} -> (A -> A) -> A
-- fix = \ {A} g =>
--   -- RLet is not yet implemented...
--   let omega = -- : D A -> D A =
--         (\ x => V (g (unv {A} (unF {A} x x))))
--   in unV {A} (omega (F omega))

-- data Nat : Type where
--    Zero : Nat
--    Succ : Nat -> Nat

-- fix_add : Nat -> Nat -> Nat
-- fix_add = fix [Nat -> Nat -> Nat]
--         \radd. \x. \y.
--             case x of
--               Zero   -> y
--               Succ n -> Succ (radd n y)

-- test : fix_add 5 2 = 7
-- test = Refl
