~/jendhub

def wv.ve

bend-osdev-word64@0.1.1.0 · PROOF_text.bend:33

import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W
import bend-osdev-word64@0.1.1.0/proof_value.bend as P

33def wv.ve(+h: Word(32n), +l: Word(32n)) -> {P.wv.V(32n, h, l) == W.W64.to_nat(W.W64{U32{h}, U32{l}}) : Nat}:
34  {==}

Uses (6)

Used by (1)