def from_le

bend-collections-laws-math@1.0.0.0 · spec/math/fixed.bend:242

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

242def from_le(k: Nat, xs: List<&2, Nat>) -> Maybe<&2, Nat>:
243  match k xs:
244    case 0n Nil{}:
245      Some{0n}
246    case 1n+p Con{+x, t}:
247      digit_on(from_le(p, t), C.fits(8n, x), x)
248    case _ _:
249      None{}