def word_exact

bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:106

import Base
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion

106def word_exact(+left: U32, +right: U32, equal: {True{} == Nat.is_eq(U32.to_nat(left), U32.to_nat(right)) : Bool}) -> Holds<{left == right : U32}>:
107  Holds{
108    %Conversion.word_natural_exact(left) : {_ == right : U32}
109    %Conversion.word_natural_exact(right) : {U32.from_nat(U32.to_nat(left)) == _ : U32}
110    Equal.cong(Nat, U32, U32.from_nat, U32.to_nat(left), U32.to_nat(right),
111      Lifecycle.natural_equal(U32.to_nat(left), U32.to_nat(right), equal))}