Commit 0ba83527 authored by Hai Dang's avatar Hai Dang
Browse files

Minor cleanup

parent 31b00c08
......@@ -40,7 +40,7 @@ Definition LinkState: Type := option node.
(**** GHOST STATE CONSTRUCTION -----------------------------------------------*)
(** The CMRA & functor we need. *)
(* a persistent map of from logical nodes to event ids. *)
#[local] Notation msq_qmapUR' := (gmapUR gname (agreeR (leibnizO event_id))).
#[local] Notation msq_qmapUR' := (agreeMR gname event_id).
#[local] Notation msq_qmapUR := (authUR msq_qmapUR').
(* an append-only list of nodes *)
#[local] Notation msq_linkUR := (mono_listUR (leibnizO node)).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment