CoordinateProofs.digits_step: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as CoordinateProofs
Lines 93-101 of bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&start_line=93&end_line=101

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/index_proofs.bend as Index

def digits_step(+head: Nat, +tail: List<&2, Nat>, rec: @+index: Shape.Fin(Shape.numel(tail)) -> {Shape.indices(tail, Shape.unflatten(tail, index)) == Shape.digits(tail, Shape.Fin.value(Shape.numel(tail), index)) : List<&2, Nat>}, coordinate: Shape.Fin(head) & Shape.Fin(Shape.numel(tail))) -> {Shape.indices(head <> tail, Shape.unflatten.step(head, tail, rest => Shape.unflatten(tail, rest), coordinate)) == Shape.digits(head <> tail, Shape.Fin.value(Nat.mul(head, Shape.numel(tail)), Shape.Fin.pack(head, Shape.numel(tail), coordinate))) : List<&2, Nat>}:
  (+first, +last) = coordinate
  +stride = Shape.numel(tail)
  +major = Shape.Fin.value(head, first)
  +minor = Shape.Fin.value(stride, last)
  %Equal.sym(Nat, Shape.Fin.value(Nat.mul(head, stride), Shape.Fin.pack(head, stride, (first, last))), Nat.add(Nat.mul(major, stride), minor), Index.pack_value(head, stride, first, last)) : {major <> Shape.indices(tail, Shape.unflatten(tail, last)) == Shape.digits(head <> tail, _) : List<&2, Nat>}
  %Nats.divmod_exact(major, stride, minor, Shape.Fin.bound(stride, last)) : {major <> Shape.indices(tail, Shape.unflatten(tail, last)) == Pair.fst(Nat, Nat, _) <> Shape.digits(tail, Pair.snd(Nat, Nat, _)) : List<&2, Nat>}
  %rec(last) : {major <> Shape.indices(tail, Shape.unflatten(tail, last)) == major <> _ : List<&2, Nat>}
  {==}

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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.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=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  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.bound
  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.value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=digits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=indices
  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=unflatten
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=unflatten.step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/index_proofs.bend&name=pack_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=divmod_exact