Hola,
En este ejercicio no logro ver la relación entre el constructor de listas y la sintaxis definida.
Entendiendo que las listas a utilizar son:
Inductive List : Set :=
| nullL : List
| consL : A -> List -> List.
Saludos,
Jairo.
Hola.
No es la idea usar List. Si defenís:
Inductive I :=
| skip: I
| ...
| begin_end : LI -> I
with LI :=
| nilLI: LI
| consLI: I -> LI ->LI.
Lo que se pide en el 6.2 sería (por ejemplo):
Infix "::" := consLI (at level 60, right associativity).
Saludos, Carlos