michael/blog
1
0
Fork 0
Code Issues 2 Pull requests Releases Packages 1 Wiki Activity

newline

Browse source
This commit is contained in:
Michael Zhang 2024-12-27 03:19:22 -05:00
parent d9289b88b2
commit bbfcf9c49f
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/content/posts/2024-12-16-crdt.lagda.md
View file

@ -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: