Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
572 B · 13 lines
1234567891011121314# eukhe: the proof of LAW write_writes_seen
import Baseimport ../../bend/doc_commit.bend as Cmimport ../../laws/doc_commit.bend as DocCommit
# the law write_writes_seendef pc.write_writes(+d: Maybe<&2, Nat>, +s: List<&2, Nat>, +c: Nat, kept: {Cm.unseen(d, s) == False{} : Bool}) -> {Cm.write(d, s, c) == Cm.Wt{True{}, Some{c}, Cm.saw(c, s)} : Cm.Wt}: %Equal.sym(Bool, Cm.unseen(d, s), False{}, kept) : {Cm.write.go(_, d, s, c) == Cm.Wt{True{}, Some{c}, Cm.saw(c, s)} : Cm.Wt} {==}
def DocCommit.write_writes_seen(d, s, c, kept): pc.write_writes(d, s, c, kept)