92def digestRoundConstants =
93 (eliminate
94 SHA256Schedule
95 (lambda unrestricted current : (family SHA256Schedule) . (family StdList Nat))
96 sha256RoundConstants
97 (branch SHA256ScheduleEnd . (constructor StdList StdListEmpty Nat))
98 (branch
99 SHA256ScheduleNext
100 head
101 tail
102 induction
103 .
104 (constructor StdList StdListCons Nat (modelWord32ToNatural 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.