~/jendhub

def word

stelliferous@0.0.2.0 · proofs/u32_successor.bend:140

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

140def word(+w: Word(32n)) -> Goal(U32{w}):
141  %WordEncoding.recover(31n,1n,w) : Goal(U32{_})
142  parts(WordEncoding.split(31n,1n,w))

Uses (6)

Used by (1)