~/jendhub

def word_exact

bendtorch-core@0.1.0.0 · src/tensor/matrix_index_proof.bend:18

import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndexProof
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads

18def word_exact(+number: Nat, +shape: Shape.Shape,
19  below: {Nat.is_lt(number, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
20  {U32.to_nat(U32.from_nat(number)) == number : Nat}:
21  Conversion.natural_word_exact(number, Shape.count(shape),
22    %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.logical_numel(Shape.dimensions(shape)), Reads.count_exact(shape)) :
23      {Nat.is_le(number, _) == True{} : Bool}
24    Conversion.lt_le(number, Shape.logical_numel(Shape.dimensions(shape)), below))

Uses (14)

Used by (10)