[Práctico 3] Ejercicio 7.4. Segundo AND

[Práctico 3] Ejercicio 7.4. Segundo AND

de Guillermo Urrutia Pereira -
Número de respuestas: 3

Hola,

Se nos ocurrió definir el AND de la siguiente forma:

Definition And2 (m n:Bool) : Bool := if m (if n t f) f.

No entendemos por qué nos está dando error de sintaxis:
Syntax error: [return_type] expected after [constr:operconstr level 200] (in [constr:binder_constr]).

Nos pasa en general con if's anidados, por ejemplo Check if t (if t f t) f.

Saludos

En respuesta a Guillermo Urrutia Pereira

Re: [Práctico 3] Ejercicio 7.4. Segundo AND

de Fernando Daniel Medina Suarez -

Yo lo hice igual que ustedes y no me da error.

Me parece que estas usando el if nativo de coq (if), en vez de usar el If que definiste mas arriba.

Saludos!