AlphaGitHub
Source/Packages

Std.Word

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

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

def · lines 341–358

stdU32IsZero

Full file
U32 comparison primitives (L11k). Model.Word32 is frozen and lacks them, so they are built here over its four byte fields (field 0 = low byte, field 3 = high byte, the carry direction of modelWord32Add) with the core byte ops.
341def stdU32IsZero =
342  (lambda unrestricted value : (family ModelWord32) .
343    (eliminate
344      ModelWord32
345      (lambda unrestricted current : (family ModelWord32) . Nat)
346      value
347      (branch
348        ModelWord32Value
349        b0
350        b1
351        b2
352        b3
353        .
354        (stdFlagAnd
355          (byte-equal b0 (byte 0))
356          (stdFlagAnd
357            (byte-equal b1 (byte 0))
358            (stdFlagAnd (byte-equal b2 (byte 0)) (byte-equal b3 (byte 0))))))))

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.