Drop the first `index` nodes of a schedule, returning the suffix that begins
at that index (or the empty schedule when the index runs past the end).
This is a FIRST-ORDER fold: the accumulator is a `SHA256Schedule` VALUE, not a
function. At each step it destructures the current suffix and keeps the tail --
a shared sub-structure of the original list, no copy -- so producing the
index-th suffix costs O(index) constant-work steps. (The list-recursion
hypothesis `nodeInduction` is deliberately unused, so it is never materialized.)
170def sha256ScheduleDrop =
171 (lambda unrestricted index : Nat .
172 (lambda unrestricted schedule : (family SHA256Schedule) .
173 (nat-eliminate
174 (lambda unrestricted current : Nat . (family SHA256Schedule))
175 schedule
176 (lambda unrestricted predecessor : Nat .
177 (lambda unrestricted induction : (family SHA256Schedule) .
178 (eliminate
179 SHA256Schedule
180 (lambda unrestricted current : (family SHA256Schedule) . (family SHA256Schedule))
181 induction
182 (branch SHA256ScheduleEnd . (constructor SHA256Schedule SHA256ScheduleEnd))
183 (branch SHA256ScheduleNext word tail nodeInduction . tail))))
184 index)))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.