scalars j from `first` below `last` from the constant bank into R18 + j
118def ahScalarsRange = (lambda unrestricted first : Nat . (lambda unrestricted last : Nat . (lambda unrestricted tail : (family SM86Program) .
119 (saFor (naturalSaturatingSubtract last first)
120 (lambda unrestricted j : Nat .
121 (saMovConst (naturalAdd 18 (naturalAdd first j)) (ahScalar (naturalAdd first j))))
122 tail))))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.