No entiendo la relación entre el constructor de listas y la sintaxis requerida. Tenemos que usar listas para implementar LIntrs?
Hola.
Instr puede ser definida de manera mutuamente inductiva con LInstr (como los árboles finitarios con las forestas/bosques):
Inductive
Instr :=
| sentenciaSkip: Instr
| sentenciaAsign: Var -> BoolExpr -> Instr
| sentenciaIfElse: BoolExpr -> Instr-> Instr->Instr
...
| sentenciaBegin : LInstr -> Instr
with LInstr :=
| nilI: LInstr
| consLI: Instr -> LInstr ->LInstr.
Saludos, Carlos