def fits_of

bendtorch-core@0.1.0.0 · src/shape/coordinate_proofs.bend:122

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

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