BoundaryProofs.decode_indices: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as BoundaryProofs
Lines 102-112 of bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&start_line=102&end_line=112

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

def decode_indices(+dims: List<&2, Nat>, +coordinate: Shape.Coordinate(dims)) -> {Some{coordinate} == Laws.decode(dims, Shape.indices(dims, coordinate)) : Maybe<&2, Shape.Coordinate(dims)>}:
  match dims:
    case Nil{}:
      match coordinate:
        case Unit{}:
          {==}
    case +head <> +tail:
      Shape.CStep{+index, +rest} = coordinate
      %decode_indices(tail, rest) : {Some{Shape.CStep{index, rest}} == Laws.decode.step(head, tail, _, Laws.fin_of(head, Shape.Fin.value(head, index))) : Maybe<&2, Shape.Coordinate(head <> tail)>}
      %fin_of_value(head, index) : {Some{Shape.CStep{index, rest}} == Laws.decode.step(head, tail, Some{rest}, _) : Maybe<&2, Shape.Coordinate(head <> tail)>}
      {==}

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=Unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=decode
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=decode.step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=fin_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=fin_of_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Coordinate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Coordinate.Step
  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=indices