~/jendhub

def full_loop

bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:722

import bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend as GradientPROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformProof
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion

722def full_loop(+shape: Shape.Shape) -> {Nat.is_le(Nat.add(Shape.elements(shape), 0n), Shape.elements(shape)) == True{} : Bool}:
723  %Equal.sym(Nat, Nat.add(Shape.elements(shape), 0n), Shape.elements(shape), TransformProof.add_zero_right(Shape.elements(shape))) :
724    {Nat.is_le(_, Shape.elements(shape)) == True{} : Bool}
725  Conversion.le_reflexive(Shape.elements(shape))

Uses (9)

Used by (1)