Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
1.0 kB · 25 lines
1234567891011121314151617181920212223242526# eukhe: lemmas the proofs of two or more areas share: string
import Baseimport ../../bend/wire.bend as Wrimport ./logic/string.bend as LLogicStringimport ./logic/wire.bend as LLogicWire
# turning a around onto acc, then all of it around onto rest, puts a before restdef wr_rev_rev(a: String, -acc: String, -rest: String) -> {String.reverse.go(String.reverse.go(a, acc), rest) == String.reverse.go(acc, LLogicString.wr_app(a, rest)) : String}: match a: case SNil{}: {==} case SCon{c, t}: wr_rev_rev(t, SCon{c, acc}, rest)
# the reference reads back the chars of adef wr_take_rt(+a: String, -rest: String) -> {LLogicWire.wo_take(String.length(a), LLogicString.wr_app(a, rest)) == Wr.Got{a, rest} : Wr.Dec<String>}: match a: case SNil{}: {==} case SCon{c, +t}: %Equal.sym(Wr.Dec<String>, LLogicWire.wo_take(String.length(t), LLogicString.wr_app(t, rest)), Wr.Got{t, rest}, wr_take_rt(t, rest)) : {LLogicWire.wo_take_cons(c, _) == Wr.Got{SCon{c, t}, rest} : Wr.Dec<String>} {==}