def lall_fail

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:273

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int.bend as U32int
import Base
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I

273def lall_fail(xs: List<&2, U32>, +e: NM.NumError) -> {G.lcm_all_go(~U32, ~I.u32_op, ~I.u32_is, xs, Fail{e}) == Fail{e} : Result<&2, &2, NM.NumError, U32>}:
274  match xs:
275    case Nil{}:
276      {==}
277    case Con{x, t}:
278      {==}

Uses (7)

Used by (0)

No other definition uses this definition.