def fit_values_spec

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

import Base

460def fit_values_spec(+dims: List<&2, U32>, +values: List<&2, Nat>) -> {fit_values(dims, values) == fit(naturals(dims), values) : Bool}:
461  match dims values:
462    case Nil{} Nil{}:
463      {==}
464    case +dh <> +dt +vh <> +vt:
465      Equal.cong(Bool, Bool, rest => Bool.and(Nat.is_lt(vh, U32.to_nat(dh)), rest), fit_values(dt, vt), fit(naturals(dt), vt), fit_values_spec(dt, vt))
466    case Nil{} vh <> vt:
467      {==}
468    case dh <> dt Nil{}:
469      {==}