Buenas, estoy un poco perdido sobre cómo definir la función update.
No entiendo bien cómo definir la salida de update diciendo lo que vale para cada elemento.
Se me ocurre hacer un fixpoint auxiliar pero capaz es un poco desprolijo.
Saludos,
Joaquín
Hola.
Todo depende de como hayas definido la Memoria. Si es una función de Var en Valor, entonces update se puede definir como una función (no recursiva) de la siguiente manera:
Definition update var val mem :=
fun var' => if beq_nat var var' then val else lookup var' mem.
Esto es, la función retorna una memoria que asigna a cada variable el valor que tenía en la memoria parámetro, salvo para la variable (var) donde la memoria se actualiza (con val).
Saludos, Carlos
Gracias!
No se me había ocurrido usar una función lambda.