U32Shift.double_word: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/u32_shift.bend as U32Shift
Lines 99-101 of stelliferous@0.0.2.0/proofs/u32_shift.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/u32_shift.bend&start_line=99&end_line=101

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

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

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_shift.bend&name=DoubleGoal
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_shift.bend&name=double_parts
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_encoding.bend&name=recover
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_encoding.bend&name=split