IndexProofs.pack_value: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as IndexProofs
Lines 71-82 of bendtorch-core@0.1.0.0/src/shape/index_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/index_proofs.bend&start_line=71&end_line=82

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

def pack_value(+a: Nat, +b: Nat, +first: Shape.Fin(a), +last: Shape.Fin(b)) -> {Shape.Fin.value(Nat.mul(a, b), Shape.Fin.pack(a, b, (first, last))) == Nat.add(Nat.mul(Shape.Fin.value(a, first), b), Shape.Fin.value(b, last)) : Nat}:
  match a:
    case 0n:
      match first:
    case 1n+p:
      match first:
        case Shape.FZero{}:
          left_value(b, Nat.mul(p, b), last)
        case Shape.FNext{+previous}:
          %add_assoc(b, Nat.mul(Shape.Fin.value(p, previous), b), Shape.Fin.value(b, last)) : {Shape.Fin.value(Nat.add(b, Nat.mul(p, b)), Shape.Fin.shift(b, Nat.mul(p, b), Shape.Fin.pack(p, b, (previous, last)))) == _ : Nat}
          %pack_value(p, b, previous, last) : {Shape.Fin.value(Nat.add(b, Nat.mul(p, b)), Shape.Fin.shift(b, Nat.mul(p, b), Shape.Fin.pack(p, b, (previous, last)))) == Nat.add(b, _) : Nat}
          shift_value(b, Nat.mul(p, b), Shape.Fin.pack(p, b, (previous, last)))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.Step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.pack
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.shift
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/index_proofs.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/index_proofs.bend&name=left_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/index_proofs.bend&name=shift_value