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