256def nativeTelemetryCounterFromNatural =
257 (lambda unrestricted value : Nat .
258 (app
259 (lambda unrestricted encoded : (family ModelWord32) .
260 (nat-eliminate
261 (lambda unrestricted exact : Nat . (family NativeTelemetryCounterResult))
262 (constructor
263 NativeTelemetryCounterResult
264 NativeTelemetryCounterFailed
265 (constructor NativeTelemetryErrorCode NativeTelemetryCounterOverflow)
266 value)
267 (lambda unrestricted exactPredecessor : Nat .
268 (lambda unrestricted ignoredExact : (family NativeTelemetryCounterResult) .
269 (constructor
270 NativeTelemetryCounterResult
271 NativeTelemetryCounterSucceeded
272 (nativeTelemetryWord32ToWord64 encoded))))
273 (naturalEqual (modelWord32ToNatural encoded) value)))
274 (modelWord32FromNaturalTruncated value)))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.