def decode_unfit

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

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

71def decode_unfit(+dims: List<&2, Nat>, +values: List<&2, Nat>, misses: {False{} == Shape.fit(dims, values) : Bool}) -> {None{} == Laws.decode(dims, values) : Maybe<&2, Shape.Coordinate(dims)>}:
72  match dims values:
73    case Nil{} Nil{}:
74      Empty.absurd({None{} == Laws.decode(Nil{}, Nil{}) : Maybe<&2, Shape.Coordinate(Nil{})>}, Shape.clash(Equal.sym(Bool, False{}, True{}, misses)))
75    case +dh <> +dt +vh <> +vt:
76      decode_unfit.step(dh, dt, vh, vt, Shape.bool_case(Nat.is_lt(vh, dh)), misses, rest => decode_unfit(dt, vt, rest))
77    case Nil{} vh <> vt:
78      {==}
79    case dh <> dt Nil{}:
80      {==}