def from_nat
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as Numericimport Base
import bend-collections-laws-math@1.0.0.0/spec/lib/numeric.bend as W
32def from_nat(n: Nat, +value: Nat) -> Word(n):
33 W.from_nat(n, value)
Uses (3)
Used by (44)
- bend-collections-laws-math@1.0.0.0/proofs/lib/u32:injective
- bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition:reconstruct
- bend-collections-laws-math@1.0.0.0/proofs/lib/u32:to_nat_from_nat
- bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition:increment_refines
- bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_addition:refines
- …