PlanProofs.align_complete: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProofs
Lines 136-154 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=136&end_line=154

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

def align_complete(+left: List<&2, U32>, +right: List<&2, U32>, +output: List<&2, Nat>, +aligned: Shape.Aligned(Shape.naturals(left), Shape.naturals(right), output)) -> {Some{output} == aligned_output(left, right, Shape.align(left, right)) : Maybe<&2, List<&2, Nat>>}:
  match left right output:
    case Nil{} Nil{} Nil{}:
      {==}
    case +lh <> +lt +rh <> +rt +oh <> +ot:
      Shape.AStep{+axis, +tail} = aligned
      align_step_complete(lh, lt, rh, rt, oh, ot, Shape.align(lt, rt), Shape.axis_choice(lh, rh), align_complete(lt, rt, ot, tail), axis_complete(lh, rh, oh, axis))
    case Nil{} Nil{} oh <> ot:
      match aligned:
    case Nil{} rh <> rt Nil{}:
      match aligned:
    case lh <> lt Nil{} Nil{}:
      match aligned:
    case Nil{} rh <> rt oh <> ot:
      match aligned:
    case lh <> lt Nil{} oh <> ot:
      match aligned:
    case lh <> lt rh <> rt Nil{}:
      match aligned:

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Aligned
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Aligned.Step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=align
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=axis_choice
  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/plan_proofs.bend&name=align_step_complete
  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=axis_complete