AlphaGitHub
Source/Packages

Std.Word

packages/foundation/standard/src/Std/Word.alpha

1,783 lines192 declarations64.2 KiBSHA-256 27bf8c3f30ee
Download exact fileView at revision3c600751929f56cd01

def · lines 365–382

stdU32HighBit

Full file
the sign bit of the high byte (1 = the byte is >= 128)
365def stdU32HighBit =
366  (lambda unrestricted value : (family ModelWord32) .
367    (eliminate
368      ModelWord32
369      (lambda unrestricted current : (family ModelWord32) . Nat)
370      value
371      (branch
372        ModelWord32Value
373        b0
374        b1
375        b2
376        b3
377        .
378        (nat-eliminate
379          (lambda unrestricted current : Nat . Nat)
380          (succ zero)
381          (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
382          (byte-less-than b3 (byte 128))))))

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.