Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
716 B · 24 lines
12345678910111213141516171819202122232425# eukhe: the proof of LAW commit_check_is_conflict## PROOF: by induction on the files: a changed file stops the check and# makes the edit conflict; an unchanged one is skipped by both.
import Baseimport ../../bend/doc_commit.bend as Cmimport ../../laws/doc_commit.bend as DocCommit
def dcw.go(fs: List<&2, Cm.Doc>, +n: Nat) -> {DocCommit.sp_go(Cm.check.go(DocCommit.sp_mets(fs), n)) == Bool.not(Cm.conflict(fs)) : Bool}: match fs: case Nil{}: {==} case f <> rest: match f: case Cm.Doc{k, c, x}: match c: case True{}: {==} case False{}: dcw.go(rest, 1n+n)
def DocCommit.commit_check_is_conflict(fs): dcw.go(fs, 0n)