def increment_below_exact

bendtorch-core@0.1.0.0 · src/tensor/word_conversion.bend:60

import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as WordConversion

import Base

60def increment_below_exact(+word: U32, +limit: U32, below: {U32.is_lt(word, limit) == True{} : Bool}) ->
61  {U32.to_nat(U32.inc(word)) == 1n+U32.to_nat(word) : Nat}:
62  match word limit:
63    case U32{+w} U32{+upper}:
64      word_increment_exact(32n, w, word_lt_has_zero(32n, w, upper, below))

Uses (8)

Used by (2)