`count` consecutive registers from `register`, prepended; none from RZ
84def sm86RegisterRun =
85 (lambda unrestricted register : (family SM86Register) .
86 (lambda unrestricted count : Nat .
87 (lambda unrestricted rest : (family StdList Nat) .
88 (let unrestricted index = (sm86RegisterIndex register) in
89 (nat-eliminate
90 (lambda unrestricted current : Nat . (family StdList Nat))
91 rest
92 (lambda unrestricted named : Nat . (lambda unrestricted ignored : (family StdList Nat) .
93 (nat-eliminate
94 (lambda unrestricted current : Nat . (family StdList Nat))
95 rest
96 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family StdList Nat) .
97 (constructor StdList StdListCons Nat
98 (nat-add index (nat-subtract (nat-subtract count 1) predecessor))
99 induction)))
100 count)))
101 (nat-add (nat-less-than index sm86RegisterZero) (nat-less-than sm86RegisterZero index)))))))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.