def below_one_value

stelliferous@0.0.2.0 · proofs/storage_address_bounds.bend:69

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

69def below_one_value(+index: U32,bound: {U32.is_lt(index,1) == True{} : Bool}) -> {0n == U32.to_nat(index) : Nat}:
70  U32{+word} = index
71  %Equal.sym(Word(32n),word,Word.zero(32n),WordEncoding.below_one_zero(31n,word,bound)) : {0n == Word.to_nat(32n,_) : Nat}
72  {==}