Source/Packages

Model.Word32

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

492 lines41 declarations17.0 KiBSHA-256 eb985612415b

def · lines 280–287

modelWord32Multiply

Full file
280def modelWord32Multiply =
281  (lambda unrestricted left : (family ModelWord32) .
282    (lambda unrestricted right : (family ModelWord32) .
283      (eliminate
284        ModelWord32MultiplyState
285        (lambda unrestricted current : (family ModelWord32MultiplyState) . (family ModelWord32))
286        (modelWord32MultiplyStateRun left right)
287        (branch ModelWord32MultiplyStateValue multiplicand multiplier product . 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.