def lift_nat
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as Genericimport Base
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as N
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
91def lift_nat(r: Result<&2, &2, M.MathError, Nat>) -> Result<&2, &2, N.NumError, Nat>:
92 match r:
93 case Done{x}:
94 Done{x}
95 case Fail{e}:
96 Fail{err(e)}
Uses (5)
Used by (7)
- bend-collections-laws-math@1.0.0.0/spec/math/generic:Ilog.agrees
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int:ilog_fin
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int:ilog_top
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int:ilog_fin
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int:ilog_top
- …