Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
1.6 kB · 26 lines
123456789101112131415161718192021222324252627# eukhe: the proof of LAW command_unknown_runs_nothing## PROOF of LAW command_unknown_runs_nothing: the words of the line are q,# w and more (every word is spaceless); the walk over q lands on q with# its entry (B.cb_walk_root); w names no child of q by its lowercase name# (q ++ [lower w] is not declared) nor by an alias, so the search finds# none and, q taking no text, the walk stands at Lost{q, w}# (B.cb_line_miss); an unknown word stays whatever follows# (B.cb_walk_lost) and finishes as Unknown{q, w}.
import Baseimport ../../bend/command.bend as Cmdimport ../../laws/command/paths.bend as Commandimport ../base/logic/logic.bend as LLogicLogicimport ./base.bend as LA
def Command.command_unknown_runs_nothing(t, q, w, more, ok, on, shut, word, after, miss): match q: case Nil{}: LLogicLogic.cb_absurd({Cmd.resolve(t, Command.cmd_render(List.append(&2, List<&2, Nat>, Nil{}, w <> more))) == Cmd.Unknown{Nil{}, w} : Cmd.Res}, on) case Con{+x, +rest}: +qq = {x <> rest : List<&2, List<&2, Nat>>} %Equal.sym(Cmd.St, Cmd.walk(Cmd.words(Command.cmd_render(List.append(&2, List<&2, Nat>, qq, w <> more))), t, Cmd.Top{}), Cmd.walk(more, t, LA.cb_miss(t, qq, w)), LA.cb_line_miss(t, qq, w, more, ok, on, word, after, miss)) : {Cmd.finish(_, t) == Cmd.Unknown{qq, w} : Cmd.Res} %Equal.sym(Bool, Command.cmd_free(t, qq), False{}, shut) : {Cmd.finish(Cmd.walk(more, t, Cmd.step.miss(_, qq, w)), t) == Cmd.Unknown{qq, w} : Cmd.Res} %Equal.sym(Cmd.St, Cmd.walk(more, t, Cmd.Lost{qq, w}), Cmd.Lost{qq, w}, LA.cb_walk_lost(more, t, qq, w)) : {Cmd.finish(_, t) == Cmd.Unknown{qq, w} : Cmd.Res} {==}