Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
1.3 kB · 30 lines
at bend/all
12345678910111213141516171819202122232425262728293031# eukhe: the proof of LAW commit_sweep_spec## PROOF: entry by entry, the code's prefix test is the spec's# (dcw.starts); the code's prefix computes to the spec's.
import Baseimport ../../bend/doc_commit.bend as Cmimport ../../laws/doc_commit.bend as DocCommitimport ./base.bend as LA
def dcw.gone_keep(b: Bool, +n: Nat, r: List<&2, Nat>) -> {Cm.gone.put(n, r, b) == DocCommit.sp_gone.keep(b, n, r) : List<&2, Nat>}: match b: case True{}: {==} case False{}: {==}
def dcw.gone(+p: String, es: List<&2, Cm.Ent>, +n: Nat) -> {Cm.gone.go(p, es, n) == DocCommit.sp_gone(p, es, n) : List<&2, Nat>}: match es: case Nil{}: {==} case e <> +rest: match e: case Cm.Ent{+name, h}: %dcw.gone(p, rest, 1n+n) : {Cm.gone.put(n, Cm.gone.go(p, rest, 1n+n), Bool.and(Cm.starts(p, name), Bool.not(h))) == DocCommit.sp_gone.keep(Bool.and(DocCommit.sp_starts(p, name), Bool.not(h)), n, _) : List<&2, Nat>} %LA.dcw.starts(p, name) : {Cm.gone.put(n, Cm.gone.go(p, rest, 1n+n), Bool.and(Cm.starts(p, name), Bool.not(h))) == DocCommit.sp_gone.keep(Bool.and(_, Bool.not(h)), n, Cm.gone.go(p, rest, 1n+n)) : List<&2, Nat>} dcw.gone_keep(Bool.and(Cm.starts(p, name), Bool.not(h)), n, Cm.gone.go(p, rest, 1n+n))
def DocCommit.commit_sweep_spec(h, es): dcw.gone(Cm.prefix(h), es, 0n)