Source/Packages

Model.Word32

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

492 lines41 declarations17.0 KiBSHA-256 eb985612415b

def · lines 241–262

modelWord32MultiplyStep

Full file
241def modelWord32MultiplyStep =
242  (lambda unrestricted state : (family ModelWord32MultiplyState) .
243    (eliminate
244      ModelWord32MultiplyState
245      (lambda unrestricted current : (family ModelWord32MultiplyState) .
246        (family ModelWord32MultiplyState))
247      state
248      (branch
249        ModelWord32MultiplyStateValue
250        multiplicand
251        multiplier
252        product
253        .
254        (constructor
255          ModelWord32MultiplyState
256          ModelWord32MultiplyStateValue
257          (modelWord32ShiftLeftOne multiplicand)
258          (modelWord32ShiftRightOne multiplier)
259          (modelWord32Select
260            (modelWord32LeastBit multiplier)
261            (modelWord32Add product multiplicand)
262            product)))))

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.