Consultas de Práctico

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