def double_word

stelliferous@0.0.2.0 · proofs/u32_shift.bend:99

import stelliferous@0.0.2.0/proofs/u32_shift.bend as U32Shift

import Base
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

99def double_word(+w: Word(32n)) -> DoubleGoal(w):
100  %WordEncoding.recover(31n,1n,w) : DoubleGoal(_)
101  double_parts(WordEncoding.split(31n,1n,w))

Uses (5)

Used by (1)

stelliferous@0.0.2.0/proofs/u32_shift:double