one past the last register the allocation names (the end of W'):
15 + k + 3m + 3mk
137def linearStepSM86RegisterSpanFor =
138 (lambda unrestricted m : Nat . (lambda unrestricted k : Nat . (lsRegWp k m m 0)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.