589def stdF32UnitStep =
590 (lambda unrestricted state : (family StdF32UnitState) .
591 (eliminate
592 StdF32UnitState
593 (lambda unrestricted current : (family StdF32UnitState) . (family StdF32UnitState))
594 state
595 (branch
596 StdF32UnitStateOf
597 current
598 shifts
599 .
600 (nat-eliminate
601 (lambda unrestricted current2 : Nat . (family StdF32UnitState))
602 (constructor StdF32UnitState StdF32UnitStateOf current shifts)
603 (lambda unrestricted predecessor : Nat .
604 (lambda unrestricted induction : (family StdF32UnitState) .
605 (constructor
606 StdF32UnitState
607 StdF32UnitStateOf
608 (stdU32ShiftLeft current (succ zero))
609 (succ shifts))))
610 (stdU32LessThan current stdF32UnitLeadingBit)))))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.