After a lovely time with mfix making cyclic data structures, so that Nat knows about its bits which are typed in terms of Nat, I then had a horrid time chasing down a peculiar bug. It turns out that
(t :->> w) @@ e = t @@ e :->> w @@ e
ain’t the same as
(t :->> w) @@ e = (t @@ e) :->> (w @@ e)
which is what I meant. Differently grouped, it loops rather tightly. Took me ages to find it. Now that I’ve nailed that little sod, I can confirm that 2+2 is indeed 4.
I’ll commit the changes tomorrow, when I’ve yanked out all the tracing.