Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
1.2 kB · 31 lines
1234567891011121314151617181920212223242526272829303132# eukhe: the proof of LAW path_resolves_inside
import Baseimport ../../bend/tools.bend as Tlimport ../../laws/tools.bend as Toolsimport ../base/logic/logic.bend as LLogicLogicimport ./base.bend as LA
# a walk that stays under its root, from the names at, is Somedef pl.ins(segs: List<&2, Tl.Seg>, at: List<&2, Nat>, h: {Tl.stays(segs, LA.pl.len(at)) == True{} : Bool}) -> {Maybe.is_some(&2, List<&2, Nat>, Tl.walk(segs, at)) == True{} : Bool}: match segs: case Nil{}: {==} case s <> rest: match s: case Tl.Name{n}: pl.ins(rest, n <> at, h) case Tl.Here{}: pl.ins(rest, at, h) case Tl.Up{}: match at: case Nil{}: LLogicLogic.tools.pl.absurdF({Maybe.is_some(&2, List<&2, Nat>, Tl.walk(Tl.Up{} <> rest, Nil{})) == True{} : Bool}, h) case a <> above: pl.ins(rest, above, h)
def pl.path_resolves_inside(+segs: List<&2, Tl.Seg>, inside: {Tl.stays(segs, 0n) == True{} : Bool}) -> {Maybe.is_some(&2, List<&2, Nat>, Tl.resolve(segs)) == True{} : Bool}: pl.ins(segs, Nil{}, inside)
def Tools.path_resolves_inside(segs, inside): pl.path_resolves_inside(segs, inside)