From bbfcf9c49fd755f808cdd4387cc7f8d2bdbed2d9 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Fri, 27 Dec 2024 03:19:22 -0500 Subject: [PATCH] newline --- src/content/posts/2024-12-16-crdt.lagda.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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: