CoordinateProofs.fits_of: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as CoordinateProofs
Lines 122-131 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=122&end_line=131

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

def fits_of(+dims: List<&2, Nat>, +values: List<&2, Nat>, ok: {True{} == Shape.fit(dims, values) : Bool}) -> Fits(dims, values):
  match dims values:
    case Nil{} Nil{}:
      Unit{}
    case +dh <> +dt +vh <> +vt:
      fits_of.step(dh, dt, vh, vt, Shape.bool_case(Nat.is_lt(vh, dh)), ok, rest => fits_of(dt, vt, rest))
    case Nil{} vh <> vt:
      Empty.absurd(Fits(Nil{}, vh <> vt), Shape.clash(ok))
    case dh <> dt Nil{}:
      Empty.absurd(Fits(dh <> dt, Nil{}), Shape.clash(ok))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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.is_lt
  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/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_of.step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=bool_case
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=clash
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=fit