[Práctico 5] Ejercicio 6.2

[Práctico 5] Ejercicio 6.2

de Jairo Yamil Bonanata Silva -
Número de respuestas: 1

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.

En respuesta a Jairo Yamil Bonanata Silva

Re: [Práctico 5] Ejercicio 6.2

de Carlos Luna -

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