law native_encoding

stelliferous@0.0.2.0 · proofs/word_arithmetic.bend:118

import Base

118law native_encoding:
119  for +a: Nat
120  {U32.from_nat(a) == U32{encode(a,32n)} : U32}