def decode_indices

bendtorch-core@0.1.0.0 · src/shape/boundary_proofs.bend:102

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

102def decode_indices(+dims: List<&2, Nat>, +coordinate: Shape.Coordinate(dims)) -> {Some{coordinate} == Laws.decode(dims, Shape.indices(dims, coordinate)) : Maybe<&2, Shape.Coordinate(dims)>}:
103  match dims:
104    case Nil{}:
105      match coordinate:
106        case Unit{}:
107          {==}
108    case +head <> +tail:
109      Shape.CStep{+index, +rest} = coordinate
110      %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)>}
111      %fin_of_value(head, index) : {Some{Shape.CStep{index, rest}} == Laws.decode.step(head, tail, Some{rest}, _) : Maybe<&2, Shape.Coordinate(head <> tail)>}
112      {==}