def wp.of_halves

bend-osdev-word64@0.1.1.0 · PROOF.bend:94

import bend-osdev-word64@0.1.1.0/PROOF.bend as PROOF

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W

94def wp.of_halves(p: Word(32n) & Word(32n)) -> W.W64:
95  (h, l) = p
96  W.W64{U32{h}, U32{l}}

Uses (5)

Used by (1)

bend-osdev-word64@0.1.1.0/LAWS:value_eq