def bad_res

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixgen.bend:141

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM

141# and it failed exactly when n does not fit
142def bad_res(~T: Data, ~of: Nat -> T, +w: Nat, +n: Nat, +r: Result<&2, &2, NM.NumError, T>, +hr: {r == SG.checked(~T, ~of, w, n) : Result<&2, &2, NM.NumError, T>}, +ok: Bool, +hok: {C.fits(w, n) == ok : Bool}) -> {F.res_bad(T, r) == Bool.not(ok) : Bool}:
143  match ok:
144    case True{}:
145      %Equal.sym(Result<&2, &2, NM.NumError, T>, r, SG.checked(~T, ~of, w, n), hr) : {F.res_bad(T, _) == False{} : Bool}
146      %Equal.sym(Bool, C.fits(w, n), True{}, hok) : {F.res_bad(T, SG.checked_pick(~T, ~of, n, _)) == False{} : Bool}
147      {==}
148    case False{}:
149      %Equal.sym(Result<&2, &2, NM.NumError, T>, r, SG.checked(~T, ~of, w, n), hr) : {F.res_bad(T, _) == True{} : Bool}
150      %Equal.sym(Bool, C.fits(w, n), False{}, hok) : {F.res_bad(T, SG.checked_pick(~T, ~of, n, _)) == True{} : Bool}
151      {==}