Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
533 B · 14 lines
123456789101112131415# eukhe: the proof of LAW command_space_lead## PROOF of LAW command_space_lead: a leading space splits off an empty# first word (words of 32 <> line is Nil <> words(line)), and the walk# skips an empty word at the root (step.empty of Top is Top), so the# walk over the words of the spaced line is the walk over the words of# the line itself: both sides compute to the same term.
import Baseimport ../../bend/command.bend as Cmdimport ../../laws/command/paths.bend as Command
def Command.command_space_lead(t, line): {==}