Buen dia.
Estamos trancados hace dias en la parte de definir "Succ", la letra dice que el dominio es N -> N, definimos Succ := func (n:N) (f:N->N) => f n
El tema es que no es el dominio no es el mismo.
Alguna sugerencia como para guiarnos ??
Gracias!
Hola.
para entender los numerales de Church, recomiendo primero leer:
http://www.cs.rice.edu/~javaplt/311/Readings/supplemental.pdf.
Teniendo en cuenta (de la letra del práctico):
Definition N := forall X : Set, X -> (X -> X) ->
X.
Definition Zero (X : Set) (o : X) (f : X -> X) := o.
Definition Uno (X : Set) (o : X) (f : X -> X) := f (Zero
X o f).
Dos podría ser:
Definition Dos (X : Set) (o : X) (f : X -> X) := f (Uno X o
f).
Luego,
Definition Succ : N -> N :=
fun (n:N) (X:Set) (o:X) (f:X->X) => f (n X o
f).
Saludos, Carlos