Muchas gracias por la explicación. Muy claro.
Acá va un intento. No sé si es válido porque la g es casi el factorial y el foldN me da N.
Saludos.
g :: Nat -> (Nat,Nat)
g Zero = (Zero, Succ Zero)
g (Succ n) = ( n' , prod (Succ n) n')
where (_,n') = g n
factorial3 :: Nat -> Nat
factorial3 n = snd (g (foldN Succ Zero n))
Acá va un intento. No sé si es válido porque la g es casi el factorial y el foldN me da N.
Saludos.
g :: Nat -> (Nat,Nat)
g Zero = (Zero, Succ Zero)
g (Succ n) = ( n' , prod (Succ n) n')
where (_,n') = g n
factorial3 :: Nat -> Nat
factorial3 n = snd (g (foldN Succ Zero n))