Source/Packages

Data.SHA256Schedule

packages/foundation/standard/src/Data/SHA256Schedule.alpha

257 lines29 declarations10.2 KiBSHA-256 583f3a41d503

def · lines 227–248

sha256ScheduleAppend

Full file
227def sha256ScheduleAppend =
228  (lambda unrestricted schedule : (family SHA256Schedule) .
229    (lambda unrestricted word : (family ModelWord32) .
230      (eliminate
231        SHA256Schedule
232        (lambda unrestricted current : (family SHA256Schedule) . (family SHA256Schedule))
233        schedule
234        (branch
235          SHA256ScheduleEnd
236          .
237          (constructor
238            SHA256Schedule
239            SHA256ScheduleNext
240            word
241            (constructor SHA256Schedule SHA256ScheduleEnd)))
242        (branch
243          SHA256ScheduleNext
244          head
245          tail
246          induction
247          .
248          (constructor SHA256Schedule SHA256ScheduleNext head induction)))))

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.