Buenas
Estoy teniendo problema para hacer la traduccion de las pre y post condiciones para las distintas acciones ya que los mappings dentro de State son parciales.
Por ejemplo, para la precondicion de Read al traducir
is_RW((s.memory[ma]).page_content
en Coq tuve que escribir
match (memory s) ma with
| None => False
| Some p => is_RW (page_content p)
end
Quería consultar si hay una manera prolija/entendible para trabajar con los retornos opcionales y evitar estar haciendo constantemente matchs.
Saludos, Tomás.