~/jendhub

def u32_unit_nat

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

import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as WordConversion
import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model

551def u32_unit_nat(+bit: Nat, below: {Nat.is_lt(bit, 32n) == True{} : Bool}) ->
552  {Model.capacity(bit) == U32.to_nat(U32{Arith.unit(32n, bit)}) : Nat}:
553  Arith.unit_nat(32n, bit, below)

Uses (8)

Used by (1)