def inside_le

bendtorch-core@0.1.0.0 · src/tensor/matmul_PROOF.bend:659

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

659def inside_le(+index: Nat, +limit: Nat, inside: {Nat.is_lt(index, limit) == True{} : Bool}) -> {Nat.is_le(index, limit) == True{} : Bool}:
660  match index limit:
661    case 0n 0n:
662      Empty.absurd({True{} == True{} : Bool}, Arith.clash(inside))
663    case 0n 1n+q:
664      {==}
665    case 1n+p 0n:
666      Empty.absurd({False{} == True{} : Bool}, Arith.clash(inside))
667    case 1n+p 1n+q:
668      inside_le(p, q, inside)