BoundaryProofs.decode_fit: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as BoundaryProofs
Lines 48-60 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=48&end_line=60

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

def decode_fit(+dims: List<&2, Nat>, +values: List<&2, Nat>, +fits: Coordinates.Fits(dims, values)) -> {Laws.decode(dims, values) == Some{Coordinates.coordinate_of(dims, values, fits)} : Maybe<&2, Shape.Coordinate(dims)>}:
  match dims values:
    case Nil{} Nil{}:
      {==}
    case +dh <> +dt +vh <> +vt:
      Coordinates.FStep{+bound, +tail} = fits
      %Equal.sym(Maybe<&2, Shape.Coordinate(dt)>, Laws.decode(dt, vt), Some{Coordinates.coordinate_of(dt, vt, tail)}, decode_fit(dt, vt, tail)) : {Laws.decode.step(dh, dt, _, Laws.fin_of(dh, vh)) == Some{Shape.CStep{Coordinates.fin_from(dh, vh, bound), Coordinates.coordinate_of(dt, vt, tail)}} : Maybe<&2, Shape.Coordinate(dh <> dt)>}
      %Equal.sym(Maybe<&2, Shape.Fin(dh)>, Laws.fin_of(dh, vh), Some{Coordinates.fin_from(dh, vh, bound)}, fin_of_from(dh, vh, bound)) : {Laws.decode.step(dh, dt, Some{Coordinates.coordinate_of(dt, vt, tail)}, _) == Some{Shape.CStep{Coordinates.fin_from(dh, vh, bound), Coordinates.coordinate_of(dt, vt, tail)}} : Maybe<&2, Shape.Coordinate(dh <> dt)>}
      {==}
    case Nil{} vh <> vt:
      match fits:
    case dh <> dt Nil{}:
      match fits:

Uses (15):
  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=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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_from
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=Fits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=Fits.Step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=coordinate_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=fin_from
  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