Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
718 B · 27 lines
at bend/all
12345678910111213141516171819202122232425262728# eukhe: the proof of LAW commit_check_spec## PROOF: file by file, the code's check from index n is the spec's.
import Baseimport ../../bend/doc_commit.bend as Cmimport ../../laws/doc_commit.bend as DocCommit
def dcw.check(ms: List<&2, Cm.Met>, +n: Nat) -> {Cm.check.go(ms, n) == DocCommit.sp_check(ms, n) : Cm.Check}: match ms: case Nil{}: {==} case m <> rest: match m: case Cm.Met{c, t}: match c: case True{}: {==} case False{}: match t: case True{}: {==} case False{}: dcw.check(rest, 1n+n)
def DocCommit.commit_check_spec(ms): dcw.check(ms, 0n)