def last_wrapped

bendtorch-core@0.1.0.0 · src/tensor/signed_PROOF.bend:101

import Base
import bendtorch-core@0.1.0.0/src/tensor/signed.bend as Signed

101def last_wrapped(+limit: U32, +k: U32, +inside: {U32.is_lt(k, limit) == True{} : Bool}) ->
102  {Nat.add(U32.to_nat(Signed.wrap(limit, Signed.Last{k})), 1n+U32.to_nat(k)) == U32.to_nat(limit) : Nat}:
103  %Equal.sym(Bool, U32.is_lt(k, limit), True{}, inside) :
104    {Nat.add(U32.to_nat(Bool.pick(U32, _, U32.sub(U32.sub(limit, 1), k), limit)), 1n+U32.to_nat(k)) == U32.to_nat(limit) : Nat}
105  last_inside(limit, k, inside)