def equal_values

stelliferous@0.0.2.0 · proofs/storage_address_bounds.bend:74

import Base
import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as Arithmetic

74def equal_values(+left: U32,+right: U32,equation: {U32.to_nat(left) == U32.to_nat(right) : Nat}) -> {left == right : U32}:
75  %Arithmetic.native_roundtrip(left) : {_ == right : U32}
76  %Arithmetic.native_roundtrip(right) : {U32.from_nat(U32.to_nat(left)) == _ : U32}
77  Equal.cong(Nat,U32,U32.from_nat,U32.to_nat(left),U32.to_nat(right),equation)