Source/Packages

Model.Word32

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

492 lines41 declarations17.0 KiBSHA-256 eb985612415b

def · lines 92–155

modelWord32Add

Full file
92def modelWord32Add =
93  (lambda unrestricted left : (family ModelWord32) .
94    (lambda unrestricted right : (family ModelWord32) .
95      (eliminate
96        ModelWord32
97        (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
98        left
99        (branch
100          ModelWord32Value
101          l0
102          l1
103          l2
104          l3
105          .
106          (eliminate
107            ModelWord32
108            (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
109            right
110            (branch
111              ModelWord32Value
112              r0
113              r1
114              r2
115              r3
116              .
117              (eliminate
118                ByteAddResult
119                (lambda unrestricted current : (family ByteAddResult) . (family ModelWord32))
120                (byteAddWithCarry l0 r0 zero)
121                (branch
122                  ByteAddResultValue
123                  sum0
124                  carry0
125                  .
126                  (eliminate
127                    ByteAddResult
128                    (lambda unrestricted current : (family ByteAddResult) . (family ModelWord32))
129                    (byteAddWithCarry l1 r1 carry0)
130                    (branch
131                      ByteAddResultValue
132                      sum1
133                      carry1
134                      .
135                      (eliminate
136                        ByteAddResult
137                        (lambda unrestricted current : (family ByteAddResult) .
138                          (family ModelWord32))
139                        (byteAddWithCarry l2 r2 carry1)
140                        (branch
141                          ByteAddResultValue
142                          sum2
143                          carry2
144                          .
145                          (eliminate
146                            ByteAddResult
147                            (lambda unrestricted current : (family ByteAddResult) .
148                              (family ModelWord32))
149                            (byteAddWithCarry l3 r3 carry2)
150                            (branch
151                              ByteAddResultValue
152                              sum3
153                              carry3
154                              .
155                              (constructor ModelWord32 ModelWord32Value sum0 sum1 sum2 sum3)))))))))))))))

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.