~/jendhub

def cursor_exact

bendtorch-core@0.1.0.0 · src/tensor/construction_PROOF.bend:546

import bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend as ConstructionPROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as WordConversion

546def cursor_exact(+shape: Shape.Shape, +cursor: Nat, room: Shape.LE(cursor, Shape.elements(shape))) ->
547  {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}:
548  WordConversion.natural_word_exact(cursor, Shape.count(shape),
549    %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), WordConversion.shape_count_exact(shape)) :
550      {Nat.is_le(cursor, _) == True{} : Bool}
551    Equal.sym(Bool, True{}, Nat.is_le(cursor, Shape.elements(shape)), Nats.le_true(cursor, Shape.elements(shape), room)))

Uses (13)

Used by (1)