PlanProofs.align_step_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 123-134 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=123&end_line=134

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

def align_step_complete(-lh: U32, -lt: List<&2, U32>, -rh: U32, -rt: List<&2, U32>, -oh: Nat, -ot: List<&2, Nat>, +rest: Shape.Alignment<lt, rt>, +choice: Shape.AxisChoice<lh, rh>, rest_seen: {Some{ot} == aligned_output(lt, rt, rest) : Maybe<&2, List<&2, Nat>>}, choice_seen: {Some{oh} == choice_output(lh, rh, choice) : Maybe<&2, Nat>}) -> {Some{oh <> ot} == aligned_output(lh <> lt, rh <> rt, Shape.align.step(lh, lt, rh, rt, rest, choice)) : Maybe<&2, List<&2, Nat>>}:
  match rest:
    case Shape.Misaligned{}:
      Empty.absurd({Some{oh <> ot} == aligned_output(lh <> lt, rh <> rt, Shape.align.step(lh, lt, rh, rt, Shape.Misaligned{}, choice)) : Maybe<&2, List<&2, Nat>>}, some_none(List<&2, Nat>, ot, rest_seen))
    case Shape.Aligns{tail, aligned}:
      match choice:
        case Shape.Clashes{}:
          Empty.absurd({Some{oh <> ot} == None{} : Maybe<&2, List<&2, Nat>>}, some_none(Nat, oh, choice_seen))
        case Shape.Picks{output, axis}:
          %some_injective(Nat, oh, U32.to_nat(output), choice_seen) : {Some{oh <> ot} == Some{_ <> Shape.naturals(tail)} : Maybe<&2, List<&2, Nat>>}
          %some_injective(List<&2, Nat>, ot, Shape.naturals(tail), rest_seen) : {Some{oh <> ot} == Some{oh <> _} : Maybe<&2, List<&2, Nat>>}
          {==}

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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=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=Alignment
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=AxisChoice
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=align.step
  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=aligned_output
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&name=choice_output
  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