Adjacent high/low words let a launch schedule index a column without
reevaluating the large exact root for every scalar patch.
38def rotaryFrequencyWords =
39 (lambda unrestricted base : Nat .
40 (lambda unrestricted columns : Nat .
41 (nat-eliminate
42 (lambda unrestricted current : Nat . (family StdList Nat))
43 (constructor StdList StdListEmpty Nat)
44 (lambda unrestricted predecessor : Nat .
45 (lambda unrestricted rest : (family StdList Nat) .
46 (let unrestricted index =
47 (naturalSaturatingSubtract
48 (naturalSaturatingSubtract columns 1) predecessor) in
49 (constructor StdList StdListCons Nat
50 (rotaryFrequencyHigh base columns index)
51 (constructor StdList StdListCons Nat
52 (rotaryFrequencyLow base columns index) rest)))))
53 columns)))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.