fact: Definition update_method (n: NId)(this: State)(k: Key)(v: Val)(u: @Update Val): State := let s := store this in let r := rec this in let d := dep this in let n' := sender_node u in let d' := sender_dep u in let r' := override r n' (d' n') in let d'' := fun n => max (d n) (d' n) in let s' := override s k (entry v n' (d' n')) in (state s' r' d'').
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)