def filled_none

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

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

474# With no Inferred size, the filled sizes hold the exact product.
475def filled_none(+extents: List<&2, Signed.Extent>, +size: U32, none: {Signed.inferred_count(extents) == 0n : Nat}) ->
476  {Shape.logical_numel(Signed.filled(extents, size)) == Signed.exact_product(extents) : Nat}:
477  match extents:
478    case Nil{}:
479      {==}
480    case Signed.Exact{+extent} <> +tail:
481      Equal.cong(Nat, Nat, x => Nat.mul(U32.to_nat(extent), x), Shape.logical_numel(Signed.filled(tail, size)), Signed.exact_product(tail),
482        filled_none(tail, size, none))
483    case Signed.Inferred{} <> +tail:
484      Empty.absurd({Shape.logical_numel(Signed.filled(Signed.Inferred{} <> tail, size)) == Signed.exact_product(Signed.Inferred{} <> tail) : Nat},
485        succ_not_zero(Signed.inferred_count(tail), none))