fact: Definition put_method (n: NId)(this: State)(k: Key)(v: Val): (State * Update) := let s := store this in let r := received this in let c := clock this in let d := dep this in let c' := c + 1 in let s' := override s k (entry v n c') in let d' := [(n, c')] in let r' := override r n c' in ((state s' r' c' d'), (@update Val n c' d)).
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)