def classify_within

bendtorch-core@0.1.0.0 · src/tensor/signed_PROOF.bend:405

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/signed.bend as Signed
import bendtorch-core@0.1.0.0/src/tensor/signed_LAWS.bend as Laws

405def classify_within(+bound: Nat, +product: Nat, +p: Nat, within: {Laws.classify(bound, product) == Signed.Within{p} : Signed.Product}) ->
406  {Nat.is_le(p, bound) == True{} : Bool}:
407  match product:
408    case 0n:
409      Empty.absurd({Nat.is_le(p, bound) == True{} : Bool},
410        Arith.clash(Equal.cong(Signed.Product, Bool, is_within, Signed.ZeroProduct{}, Signed.Within{p}, within)))
411    case 1n+r:
412      within_decided(bound, r, p, within, Shape.bool_case(Nat.is_le(1n+r, bound)))