diff --git a/src/content/posts/2024-12-16-crdt.lagda.md b/src/content/posts/2024-12-16-crdt.lagda.md index 5f85af3..7ec0a94 100644 --- a/src/content/posts/2024-12-16-crdt.lagda.md +++ b/src/content/posts/2024-12-16-crdt.lagda.md @@ -96,7 +96,8 @@ module _ {ℓ cℓ timeℓ timeℓ₁ timeℓ₂ : Level} (TimeOrder : StrictTot apply2 : (o1 o2 : op) (t1 t2 : Time) → A → A -- The property that applying changes must be commutative. - comm : (a : A) → (o1 o2 : op) (t1 t2 : Time) → apply2 o1 o2 t1 t2 a ≡ apply2 o2 o1 t2 t1 a + comm : (a : A) → (o1 o2 : op) (t1 t2 : Time) + → apply2 o1 o2 t1 t2 a ≡ apply2 o2 o1 t2 t1 a ``` I think in reality it would be the job of `op` to store the time, rather than the entire `isCRDT`, but this is the way I wrote it :sob: