No logro comprender la naturaleza de Exp: Set -> Set
Exp contiene los operandos y la operación ?
Como podemos definir la operación, cuando puede ser del tipo Set->Set->Set o del tipo Set->Set ?
Agradezco cualquier guía o aclaración.
Hola.
La idea es que Exp represente la sintaxis abstracta de las expresiones:
Inductive Exp (A: Set): Set :=
id : A -> Exp A
| suma : Exp A -> Exp A -> Exp A
| ...
Luego, la parte b sería entonces:
Fixpoint val (e: Exp nat) : nat := match e with id a => a | suma a b => val a + val b (* se interpreta el constructor "suma" como la adición de nat: "+" *) | ... end.
Saludos, Carlos