Source/Packages

Model.Word32Logic

packages/foundation/standard/src/Model/Word32Logic.alpha

142 lines9 declarations4.4 KiBSHA-256 ef93d5a70a2e

def · lines 8–39

modelWord32And

Full file
8def modelWord32And =
9  (lambda unrestricted left : (family ModelWord32) .
10    (lambda unrestricted right : (family ModelWord32) .
11      (eliminate
12        ModelWord32
13        (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
14        left
15        (branch
16          ModelWord32Value
17          l0
18          l1
19          l2
20          l3
21          .
22          (eliminate
23            ModelWord32
24            (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
25            right
26            (branch
27              ModelWord32Value
28              r0
29              r1
30              r2
31              r3
32              .
33              (constructor
34                ModelWord32
35                ModelWord32Value
36                (byteAnd l0 r0)
37                (byteAnd l1 r1)
38                (byteAnd l2 r2)
39                (byteAnd l3 r3))))))))

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.