Buenas, nos surgieron varias dudas al comenzar a realizar este práctico.
- La primera de ellas es cómo hay que compilar Maps.v, ya que seguimos lo indicado en otro hilo del foro pero nos sigue saliendo un error (Coqtop died badly. Resetting).
- La segunda es qué es el tipo Value, en el paper definen a content como sigue: content = RW (v: option Value) | ... pero no sabemos a qué Value se refiere.
- Al ir bajando línea por línea en Maps.v, nos salta el siguiente error en Definition is_Value, Error: The constructor Value (in type exc) expects 2 arguments.
- Por último, entendemos que hay que definir todos los tipos participantes en State, pero no estamos seguros si lo estamos haciendo de la forma correcta. Por ejemplo definimos lo siguiente para el tipo page_owner:
Inductive page_owner :=
| Hyp
| Os : forall (osi: os_ident), page_owner
| No_Owner.
Es correcto hacerlo de dicha forma?
Gracias.