77def wordDigestFor =
78 (lambda erased A : Type 0 .
79 (lambda unrestricted count : Nat .
80 (lambda unrestricted body : (pi unrestricted index : Nat . (pi unrestricted rest : A . A)) .
81 (lambda unrestricted tail : A .
82 (nat-eliminate
83 (lambda unrestricted current : Nat . A)
84 tail
85 (lambda unrestricted predecessor : Nat .
86 (lambda unrestricted induction : A .
87 (body
88 (naturalSaturatingSubtract (naturalSaturatingSubtract count 1) predecessor)
89 induction)))
90 count)))))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.