def cursor_below

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

534def cursor_below(+cursor: Nat, +remaining: Nat, +count: Nat,
535  room: Shape.LE(Nat.add(cursor, 1n+remaining), count)) -> Shape.LT(cursor, count):
536  match cursor count:
537    case 0n 0n:
538      match room:
539    case 0n 1n+q:
540      Unit{}
541    case 1n+p 0n:
542      match room:
543    case 1n+p 1n+q:
544      cursor_below(p, remaining, q, room)