68def byteShiftRight =
69 (lambda unrestricted value : Byte .
70 (lambda unrestricted amount : Nat .
71 (nat-eliminate
72 (lambda unrestricted current : Nat . Byte)
73 (byte 0)
74 (lambda unrestricted predecessor : Nat .
75 (lambda unrestricted induction : Byte . (byte-shift-right value (nat-to-byte amount))))
76 (nat-less-than amount byteNaturalEight))))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.