SignedPROOF.filled_none: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend as SignedPROOF
Lines 474-485 of bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend&start_line=474&end_line=485

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

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

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed.bend&name=Extent
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed.bend&name=exact_product
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed.bend&name=filled
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed.bend&name=inferred_count
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend&name=succ_not_zero