Alguna idea?
Hola, estoy teniendo dificultades para entender como deben ser usados los mapeos, de hecho algo que no entiendo es que cuando hago el checkeo del tipo mapping desde Maps, me da Set y desde quienes lo importan, me da Set -> Set -> Set.
Para trabajar con mappings, pueden:
1) basarse en la biblioteca Maps.v que se incluye junto con la letra del práctico, o
2) directamente usar las funciones de Coq. Para definir una función parcial de un tipo A a un tipo B, puede usarse el tipo option:
Inductive option (T : Type) : Type :=
Some : T -> option T | None : option T
Esto es, f : A -> option B.
Volviendo a (1) copio abajo un ejemplo de uso de map_apply para definir (de cierta manera - es solo un ejemplo) la precondición de la acción chmod:
Definition PreConditionChmod (s : state) : Prop :=
aos_activity s = waiting /\
exists os,
Value _ os = map_apply os_ident_eq (oss s) (active_os s) /\
(hcall os) = None.
Saludos, Carlos