PlanProofs.complete_align: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProofs
Lines 163-171 of bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&start_line=163&end_line=171

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend as Construct
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as Laws

def complete_align(+left: Shape.Shape, +right: Shape.Shape, +left_padding: Nat, +right_padding: Nat, -minimal: Shape.PadMinimal<left_padding, right_padding>, +alignment: Shape.Alignment<Shape.pad_words(left_padding, Shape.dimensions(left)), Shape.pad_words(right_padding, Shape.dimensions(right))>, -target: List<&2, Nat>, seen: {Some{target} == aligned_output(Shape.pad_words(left_padding, Shape.dimensions(left)), Shape.pad_words(right_padding, Shape.dimensions(right)), alignment) : Maybe<&2, List<&2, Nat>>}, +rank_bound: Shape.LE(List.length(&2, Nat, target), 4n), +capacity_bound: Shape.LE(Shape.numel(target), 1048576n)) -> {Laws.broadcast_built(Shape.broadcast_checked.align(left, right, left_padding, right_padding, minimal, alignment)) == True{} : Bool}:
  match alignment:
    case Shape.Misaligned{}:
      Empty.absurd({False{} == True{} : Bool}, some_none(List<&2, Nat>, target, seen))
    case Shape.Aligns{+output, aligned}:
      +same = some_injective(List<&2, Nat>, target, Shape.naturals(output), seen)
      +rank_fits = Nats.le_rewrite(Shape.rank_dimensions(output), List.length(&2, Nat, target), 4n, Equal.trans(Nat, List.length(&2, Nat, target), List.length(&2, Nat, Shape.naturals(output)), Shape.rank_dimensions(output), Equal.cong(List<&2, Nat>, Nat, values => List.length(&2, Nat, values), target, Shape.naturals(output), same), Equal.sym(Nat, Shape.rank_dimensions(output), List.length(&2, Nat, Shape.naturals(output)), Shape.rank_naturals(output))), rank_bound)
      +capacity_fits = Nats.le_rewrite(Shape.numel(Shape.naturals(output)), Shape.numel(target), 1048576n, Equal.cong(List<&2, Nat>, Nat, values => Shape.numel(values), target, Shape.naturals(output), same), capacity_bound)
      complete_construct(left, right, left_padding, right_padding, minimal, output, Shape.broadcast_checked.repad(left_padding, right_padding, Shape.dimensions(left), Shape.dimensions(right), output, aligned), Shape.construct(output), Construct.construction_complete(output, Shape.bool_case(Nat.is_le(Shape.rank_dimensions(output), 4n)), Nats.le_true(Shape.rank_dimensions(output), 4n, rank_fits), capacity_fits))

Uses (32):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=broadcast_built
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend&name=construction_complete
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Alignment
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=LE
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=PadMinimal
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=bool_case
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=broadcast_checked.align
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=broadcast_checked.repad
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=construct
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=naturals
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=pad_words
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=rank_dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=rank_naturals
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=le_rewrite
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=le_true
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&name=aligned_output
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&name=complete_construct
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&name=some_injective
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&name=some_none