351def sha256ExpandSchedule =
352 (lambda unrestricted initialSchedule : (family SHA256Schedule) .
353 (nat-eliminate
354 (lambda unrestricted validInitialLength : Nat . (family SHA256ScheduleExpansionResult))
355 (constructor
356 SHA256ScheduleExpansionResult
357 SHA256ScheduleExpansionFailed
358 (constructor SHA256ErrorCode SHA256ScheduleLengthInvalid)
359 (sha256ScheduleLength initialSchedule))
360 (lambda unrestricted predecessor : Nat .
361 (lambda unrestricted induction : (family SHA256ScheduleExpansionResult) .
362 (sha256ValidateExpandedSchedule
363 (sha256ExpandScheduleWithFuel
364 sha256NaturalFortyEight
365 (constructor
366 SHA256ScheduleExpansionState
367 SHA256ScheduleExpansionStateValue
368 initialSchedule
369 sha256NaturalSixteen
370 zero
371 zero
372 zero
373 zero
374 zero
375 zero)))))
376 (naturalEqual (sha256ScheduleLength initialSchedule) sha256NaturalSixteen)))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.