def natural_presence

bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:579

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as Laws

579def natural_presence(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +values: List<&2, F32>,
580  -listed: Laws.Listed(Core.Packed{shape, tensor}, values), +position: Nat, -within: Shape.LE(position, 1048576n)) ->
581  Holds<{Nat.is_lt(position, List.length(&2, F32, values)) == Nat.is_lt(position, Shape.logical_numel(Shape.dimensions(shape))) : Bool}>:
582  Holds{
583    %Conversion.capacity_natural_word_exact(position, within) : {Nat.is_lt(_, List.length(&2, F32, values)) == Nat.is_lt(_, Shape.logical_numel(Shape.dimensions(shape))) : Bool}
584    {\{Holds: proof => proof} : Holds<{Nat.is_lt(U32.to_nat(U32.from_nat(position)), List.length(&2, F32, values)) == Nat.is_lt(U32.to_nat(U32.from_nat(position)), Shape.logical_numel(Shape.dimensions(shape))) : Bool}> -> {Nat.is_lt(U32.to_nat(U32.from_nat(position)), List.length(&2, F32, values)) == Nat.is_lt(U32.to_nat(U32.from_nat(position)), Shape.logical_numel(Shape.dimensions(shape))) : Bool}}(
585      same_presence(shape, tensor, values, listed, U32.from_nat(position)))}