Consecutive words taken from little-endian bytes, used for the f32 scalars a
kernel reads after its addresses.
152def bobWordPatches =
153 (lambda unrestricted words : Nat .
154 (nat-eliminate
155 (lambda unrestricted current : Nat .
156 (pi unrestricted word : Nat .
157 (pi unrestricted input : Bytes .
158 (pi unrestricted rest : (family NvidiaParameterPatches) .
159 (family NvidiaParameterPatches)))))
160 (lambda unrestricted word : Nat .
161 (lambda unrestricted input : Bytes .
162 (lambda unrestricted rest : (family NvidiaParameterPatches) . rest)))
163 (lambda unrestricted predecessor : Nat .
164 (lambda unrestricted induction :
165 (pi unrestricted word : Nat .
166 (pi unrestricted input : Bytes .
167 (pi unrestricted rest : (family NvidiaParameterPatches) .
168 (family NvidiaParameterPatches)))) .
169 (lambda unrestricted word : Nat .
170 (lambda unrestricted input : Bytes .
171 (lambda unrestricted rest : (family NvidiaParameterPatches) .
172 (eliminate
173 DataBytesWord64DecodeResult
174 (lambda unrestricted current : (family DataBytesWord64DecodeResult) .
175 (family NvidiaParameterPatches))
176 (dataBytesReadWord64LE input)
177 (branch DataBytesWord64Decoded value remaining .
178 (bobPatch word value (induction (succ word) remaining rest)))
179 (branch DataBytesWord64DecodeFailed error . rest)))))))
180 words))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.