def cpow

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix32.bend:253

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/spec/math/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int.bend as UI

253def cpow(+a: U32, +e: U32, +ok: Bool, +hok: {C.fits(32n, pw(a, e)) == ok : Bool}) -> {SF.mval(~U32, ~SG.u32_val, F.res_opt(U32, gpow(a, e))) == SF.keep(ok, pw(a, e)) : Maybe<&2, Nat>}:
254  match ok:
255    case True{}:
256      %Equal.sym(Result<&2, &2, NM.NumError, U32>, gpow(a, e), SG.checked(~U32, ~SG.u32_of, 32n, pw(a, e)), UI.pow_checked(a, vs(e))) : {SF.mval(~U32, ~SG.u32_val, F.res_opt(U32, _)) == Some{pw(a, e)} : Maybe<&2, Nat>}
257      %Equal.sym(Bool, C.fits(32n, pw(a, e)), True{}, hok) : {SF.mval(~U32, ~SG.u32_val, F.res_opt(U32, SG.checked_pick(~U32, ~SG.u32_of, pw(a, e), _))) == Some{pw(a, e)} : Maybe<&2, Nat>}
258      Equal.cong(Nat, Maybe<&2, Nat>, t => Some{t}, SG.u32_val(SG.u32_of(pw(a, e))), pw(a, e), LW.vo(pw(a, e), hok))
259    case False{}:
260      %Equal.sym(Result<&2, &2, NM.NumError, U32>, gpow(a, e), SG.checked(~U32, ~SG.u32_of, 32n, pw(a, e)), UI.pow_checked(a, vs(e))) : {SF.mval(~U32, ~SG.u32_val, F.res_opt(U32, _)) == None{} : Maybe<&2, Nat>}
261      %Equal.sym(Bool, C.fits(32n, pw(a, e)), False{}, hok) : {SF.mval(~U32, ~SG.u32_val, F.res_opt(U32, SG.checked_pick(~U32, ~SG.u32_of, pw(a, e), _))) == None{} : Maybe<&2, Nat>}
262      {==}