Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
1.2 kB · 51 lines
at main
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152# eukhe: the proof of LAW commit_outcome_spec## PROOF: every publish fact computes.
import Baseimport ../../bend/doc_commit.bend as Cmimport ../../laws/doc_commit.bend as DocCommit
def dcw.outcome(p: Cm.Pub) -> {Cm.outcome(p) == DocCommit.sp_outcome(p) : Cm.Outcome}: match p: case Cm.Updated{x}: match x: case Cm.NotPlaced{}: {==} case Cm.Placed{s}: match s: case True{}: {==} case False{}: {==} case Cm.Deleted{r}: match r: case True{}: {==} case False{}: {==} case Cm.Moved{x, r}: match x: case Cm.NotPlaced{}: match r: case True{}: {==} case False{}: {==} case Cm.Placed{s}: match s: case True{}: match r: case True{}: {==} case False{}: {==} case False{}: match r: case True{}: {==} case False{}: {==}
def DocCommit.commit_outcome_spec(p): dcw.outcome(p)