U32Shift.no_carry: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/u32_shift.bend as U32Shift
Lines 37-39 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=37&end_line=39

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

def no_carry(+w: Word(32n),+c: Bool) -> Goal(w,c):
  %WordEncoding.recover(31n,1n,w) : Goal(_,c)
  parts(c,WordEncoding.split(31n,1n,w))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Goal
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_shift.bend&name=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