317def sha256ValidateExpandedSchedule =
318 (lambda unrestricted result : (family SHA256ScheduleExpansionResult) .
319 (eliminate
320 SHA256ScheduleExpansionResult
321 (lambda unrestricted current : (family SHA256ScheduleExpansionResult) .
322 (family SHA256ScheduleExpansionResult))
323 result
324 (branch
325 SHA256ScheduleExpansionSucceeded
326 schedule
327 telemetry
328 .
329 (nat-eliminate
330 (lambda unrestricted validLength : Nat . (family SHA256ScheduleExpansionResult))
331 (constructor
332 SHA256ScheduleExpansionResult
333 SHA256ScheduleExpansionFailed
334 (constructor SHA256ErrorCode SHA256ScheduleLengthInvalid)
335 (sha256ScheduleLength schedule))
336 (lambda unrestricted predecessor : Nat .
337 (lambda unrestricted induction : (family SHA256ScheduleExpansionResult) .
338 (constructor
339 SHA256ScheduleExpansionResult
340 SHA256ScheduleExpansionSucceeded
341 schedule
342 telemetry)))
343 (naturalEqual (sha256ScheduleLength schedule) sha256NaturalSixtyFour)))
344 (branch
345 SHA256ScheduleExpansionFailed
346 error
347 failedIndex
348 .
349 (constructor SHA256ScheduleExpansionResult SHA256ScheduleExpansionFailed error failedIndex))))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.