557def magnitudeRepeatSmall =
558 (lambda erased State : Type 0 .
559 (lambda unrestricted count : Nat .
560 (lambda unrestricted step : (pi unrestricted value : State . State) .
561 (lambda unrestricted seed : State .
562 (nat-eliminate
563 (lambda unrestricted index : Nat . State)
564 seed
565 (lambda unrestricted predecessor : Nat .
566 (lambda unrestricted induction : State . (step induction)))
567 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.