50def nativeTelemetrySourceAt =
51 (lambda unrestricted values : (family NativeTelemetrySourceValues) .
52 (lambda unrestricted index : Nat .
53 (eliminate
54 NativeTelemetrySourceValues
55 (lambda unrestricted current : (family NativeTelemetrySourceValues) .
56 (family NativeTelemetrySourceWord))
57 values
58 (branch
59 NativeTelemetrySourceValuesValue
60 word0
61 word1
62 word2
63 word3
64 word4
65 word5
66 word6
67 word7
68 .
69 (aosChoose
70 (family NativeTelemetrySourceWord)
71 (naturalEqual index 0)
72 word0
73 (aosChoose
74 (family NativeTelemetrySourceWord)
75 (naturalEqual index 1)
76 word1
77 (aosChoose
78 (family NativeTelemetrySourceWord)
79 (naturalEqual index 2)
80 word2
81 (aosChoose
82 (family NativeTelemetrySourceWord)
83 (naturalEqual index 3)
84 word3
85 (aosChoose
86 (family NativeTelemetrySourceWord)
87 (naturalEqual index 4)
88 word4
89 (aosChoose
90 (family NativeTelemetrySourceWord)
91 (naturalEqual index 5)
92 word5
93 (aosChoose
94 (family NativeTelemetrySourceWord)
95 (naturalEqual index 6)
96 word6
97 (aosChoose
98 (family NativeTelemetrySourceWord)
99 (naturalEqual index 7)
100 word7
101 (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted)))))))))))))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.