bend-collections-laws-math@1.0.0.0 checks

0xf86f5f1d9a594d5a5cff999100e01d03

no description

bend-collections-laws-math@1.0.0.0 by Giulio2002

Published

2026-09-30

Size

4,146,698 bytes, 222 files

License

MIT (LICENSE)

Declarations

188 laws (188 proved), 5293 defs, 45 types

Import

import bend-collections-laws-math@1.0.0.0/laws_math.bend as Laws_math
import 0xf86f5f1d9a594d5a5cff999100e01d03/laws_math.bend as Laws_math
import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as Arith
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/arith.bend as Arith
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend as Addition
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/addition.bend as Addition
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition_bounds.bend as Addition_bounds
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/addition_bounds.bend as Addition_bounds
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/counter.bend as Counter
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/counter.bend as Counter
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_bounds.bend as Division_bounds
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/division_bounds.bend as Division_bounds
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate.bend as Division_candidate
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/division_candidate.bend as Division_candidate
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate_bound.bend as Division_candidate_bound
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/division_candidate_bound.bend as Division_candidate_bound
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_invariant.bend as Division_invariant
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/division_invariant.bend as Division_invariant
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend as Division_no_overflow
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/division_no_overflow.bend as Division_no_overflow
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend as Division_quotient
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/division_quotient.bend as Division_quotient
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_remainder.bend as Division_remainder
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/division_remainder.bend as Division_remainder
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_shift.bend as Division_shift
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/division_shift.bend as Division_shift
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_value.bend as Division_value
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/division_value.bend as Division_value
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend as Invariants
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/invariants.bend as Invariants
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_bridge.bend as Map_bridge
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_bridge.bend as Map_bridge
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_difference_order.bend as Map_difference_order
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_difference_order.bend as Map_difference_order
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_index.bend as Map_index
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_index.bend as Map_index
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_insert.bend as Map_insert
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_insert.bend as Map_insert
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_lookup.bend as Map_lookup
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_lookup.bend as Map_lookup
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_routing.bend as Map_routing
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_routing.bend as Map_routing
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition.bend as Modular_addition
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/modular_addition.bend as Modular_addition
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/modular_negation.bend as Modular_negation
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/modular_negation.bend as Modular_negation
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as Nat_algebra
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/nat_algebra.bend as Nat_algebra
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/native_map.bend as Native_map
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/native_map.bend as Native_map
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/natural_division.bend as Natural_division
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/natural_division.bend as Natural_division
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/natural_products.bend as Natural_products
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/natural_products.bend as Natural_products
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/negation_magnitude.bend as Negation_magnitude
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/negation_magnitude.bend as Negation_magnitude
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/numeric.bend as Numeric
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/numeric.bend as Numeric
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/string_compare.bend as String_compare
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/string_compare.bend as String_compare
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/subtraction_bounds.bend as Subtraction_bounds
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/subtraction_bounds.bend as Subtraction_bounds
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_addition.bend as Word_addition
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/word_addition.bend as Word_addition
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_bounds.bend as Word_bounds
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/word_bounds.bend as Word_bounds
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_comparison.bend as Word_comparison
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/word_comparison.bend as Word_comparison
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_multiplication.bend as Word_multiplication
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/word_multiplication.bend as Word_multiplication
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_shift.bend as Word_shift
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/word_shift.bend as Word_shift
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_subtraction.bend as Word_subtraction
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/word_subtraction.bend as Word_subtraction
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend as Word_value
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/word_value.bend as Word_value
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as Numeric
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bend as Numeric
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/unsigned_division.bend as Unsigned_division
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/unsigned_division.bend as Unsigned_division
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/cache.bend as Cache
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/cache.bend as Cache
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/time.bend as Time
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/time.bend as Time
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as Wide
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.bend as Wide
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/types/model.bend as Model
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.bend as Model
import bend-collections-laws-math@1.0.0.0/proofs/lib/list.bend as MList
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/list.bend as MList
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as Logic
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/logic.bend as Logic
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as MNat
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/nat.bend as MNat
import bend-collections-laws-math@1.0.0.0/proofs/lib/two_list.bend as Two_list
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/two_list.bend as Two_list
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as MU32
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/u32.bend as MU32
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as U32alg
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/u32alg.bend as U32alg
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as U32div
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/u32div.bend as U32div
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32half.bend as U32half
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/u32half.bend as U32half
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as MWord
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.bend as MWord
import bend-collections-laws-math@1.0.0.0/proofs/lib/words32.bend as Words32
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/words32.bend as Words32
import bend-collections-laws-math@1.0.0.0/proofs/math/hash/hash.bend as Hash
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/hash/hash.bend as Hash
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as Arith
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/natural/arith.bend as Arith
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend as Bits
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/natural/bits.bend as Bits
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/fact.bend as Fact
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/natural/fact.bend as Fact
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend as Gcd
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/natural/gcd.bend as Gcd
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/inverse.bend as Inverse
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/natural/inverse.bend as Inverse
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend as Lcm
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/natural/lcm.bend as Lcm
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/lists.bend as Lists
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/natural/lists.bend as Lists
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/logs.bend as Logs
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/natural/logs.bend as Logs
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/misc.bend as Misc
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/natural/misc.bend as Misc
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/modpow.bend as Modpow
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/natural/modpow.bend as Modpow
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/proof.bend as Proof
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/natural/proof.bend as Proof
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend as Roots
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/natural/roots.bend as Roots
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/sqrtn.bend as Sqrtn
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/natural/sqrtn.bend as Sqrtn
import bend-collections-laws-math@1.0.0.0/proofs/math/number/bitcount.bend as Bitcount
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/number/bitcount.bend as Bitcount
import bend-collections-laws-math@1.0.0.0/proofs/math/number/egcd.bend as Egcd
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/number/egcd.bend as Egcd
import bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend as Fixprime
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/number/fixprime.bend as Fixprime
import bend-collections-laws-math@1.0.0.0/proofs/math/number/prime.bend as Prime
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/number/prime.bend as Prime
import bend-collections-laws-math@1.0.0.0/proofs/math/number/proof.bend as Proof
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/number/proof.bend as Proof
import bend-collections-laws-math@1.0.0.0/proofs/math/pow2/pow2.bend as Pow2
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/pow2/pow2.bend as Pow2
import bend-collections-laws-math@1.0.0.0/proofs/math/proof.bend as Proof
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/proof.bend as Proof
import bend-collections-laws-math@1.0.0.0/proofs/math/random/below.bend as Below
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/below.bend as Below
import bend-collections-laws-math@1.0.0.0/proofs/math/random/bits.bend as Bits
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/bits.bend as Bits
import bend-collections-laws-math@1.0.0.0/proofs/math/random/bounded.bend as Bounded
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/bounded.bend as Bounded
import bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/block.bend as Block
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/chacha8/block.bend as Block
import bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/rounds.bend as Rounds
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/chacha8/rounds.bend as Rounds
import bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/seed.bend as Seed
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/chacha8/seed.bend as Seed
import bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/stream.bend as Stream
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/chacha8/stream.bend as Stream
import bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend as Float
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/float.bend as Float
import bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend as Fround
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/fround.bend as Fround
import bend-collections-laws-math@1.0.0.0/proofs/math/random/lemire.bend as Lemire
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/lemire.bend as Lemire
import bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/impl.bend as Impl
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/pcg/impl.bend as Impl
import bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/step.bend as Step
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/pcg/step.bend as Step
import bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/xor.bend as Xor
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/pcg/xor.bend as Xor
import bend-collections-laws-math@1.0.0.0/proofs/math/random/proof.bend as Proof
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/proof.bend as Proof
import bend-collections-laws-math@1.0.0.0/proofs/math/random/proof_draws.bend as Proof_draws
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/proof_draws.bend as Proof_draws
import bend-collections-laws-math@1.0.0.0/proofs/math/random/proof_float.bend as Proof_float
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/proof_float.bend as Proof_float
import bend-collections-laws-math@1.0.0.0/proofs/math/random/proof_pcg.bend as Proof_pcg
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/proof_pcg.bend as Proof_pcg
import bend-collections-laws-math@1.0.0.0/proofs/math/random/shuffle.bend as Shuffle
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/shuffle.bend as Shuffle
import bend-collections-laws-math@1.0.0.0/proofs/math/random/uint64n.bend as Uint64n
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/uint64n.bend as Uint64n
import bend-collections-laws-math@1.0.0.0/proofs/math/random/wrappers.bend as Wrappers
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/wrappers.bend as Wrappers
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend as Bgcdnat
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.bend as Bgcdnat
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/combnat.bend as Combnat
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/combnat.bend as Combnat
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/examples.bend as Examples
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/examples.bend as Examples
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend as F64adda
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64adda.bend as F64adda
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addb.bend as F64addb
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addb.bend as F64addb
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addc.bend as F64addc
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addc.bend as F64addc
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adde.bend as F64adde
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64adde.bend as F64adde
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf.bend as F64addf
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addf.bend as F64addf
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend as F64addg
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.bend as F64addg
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addh.bend as F64addh
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addh.bend as F64addh
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addp.bend as F64addp
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addp.bend as F64addp
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adds.bend as F64adds
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64adds.bend as F64adds
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addv.bend as F64addv
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addv.bend as F64addv
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as F64bits
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64bits.bend as F64bits
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as F64bl
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64bl.bend as F64bl
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64close.bend as F64close
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64close.bend as F64close
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as F64cmp
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64cmp.bend as F64cmp
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64conv.bend as F64conv
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64conv.bend as F64conv
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divc.bend as F64divc
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64divc.bend as F64divc
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divd.bend as F64divd
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64divd.bend as F64divd
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divf.bend as F64divf
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64divf.bend as F64divf
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divn.bend as F64divn
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64divn.bend as F64divn
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divq.bend as F64divq
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64divq.bend as F64divq
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divv.bend as F64divv
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64divv.bend as F64divv
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divx.bend as F64divx
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64divx.bend as F64divx
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64exp.bend as F64exp
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64exp.bend as F64exp
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend as F64fmod
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64fmod.bend as F64fmod
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as F64light
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64light.bend as F64light
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mexp.bend as F64mexp
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64mexp.bend as F64mexp
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64misc.bend as F64misc
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64misc.bend as F64misc
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64modf.bend as F64modf
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64modf.bend as F64modf
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mul.bend as F64mul
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64mul.bend as F64mul
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulc.bend as F64mulc
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64mulc.bend as F64mulc
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulf.bend as F64mulf
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64mulf.bend as F64mulf
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulp.bend as F64mulp
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64mulp.bend as F64mulp
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulv.bend as F64mulv
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64mulv.bend as F64mulv
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend as F64next
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64next.bend as F64next
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64norm.bend as F64norm
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64norm.bend as F64norm
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64nrp.bend as F64nrp
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64nrp.bend as F64nrp
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64ofnat.bend as F64ofnat
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64ofnat.bend as F64ofnat
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64ratio.bend as F64ratio
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64ratio.bend as F64ratio
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rint.bend as F64rint
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64rint.bend as F64rint
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as F64round
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64round.bend as F64round
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as F64rtools
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64rtools.bend as F64rtools
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqa.bend as F64sqa
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64sqa.bend as F64sqa
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend as F64sqc
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64sqc.bend as F64sqc
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqf.bend as F64sqf
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64sqf.bend as F64sqf
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqk.bend as F64sqk
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64sqk.bend as F64sqk
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqn.bend as F64sqn
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64sqn.bend as F64sqn
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqr.bend as F64sqr
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64sqr.bend as F64sqr
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqs.bend as F64sqs
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64sqs.bend as F64sqs
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqv.bend as F64sqv
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64sqv.bend as F64sqv
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqw.bend as F64sqw
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64sqw.bend as F64sqw
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqx.bend as F64sqx
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64sqx.bend as F64sqx
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as F64tools
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64tools.bend as F64tools
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix32.bend as Fix32
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/fix32.bend as Fix32
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix64.bend as Fix64
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/fix64.bend as Fix64
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbits.bend as Fixbits
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/fixbits.bend as Fixbits
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend as Fixbytes
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/fixbytes.bend as Fixbytes
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixgen.bend as Fixgen
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/fixgen.bend as Fixgen
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/float.bend as Float
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/float.bend as Float
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/montnat.bend as Montnat
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/montnat.bend as Montnat
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as Natcmp
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natcmp.bend as Natcmp
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as Natfuel
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natfuel.bend as Natfuel
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natlight.bend as Natlight
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natlight.bend as Natlight
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/shrn.bend as Shrn
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/shrn.bend as Shrn
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32.bend as MU32
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/u32.bend as MU32
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int.bend as U32int
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/u32int.bend as U32int
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as U32laws
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/u32laws.bend as U32laws
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32mont.bend as U32mont
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/u32mont.bend as U32mont
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64bgcd.bend as U64bgcd
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/u64bgcd.bend as U64bgcd
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend as U64int
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/u64int.bend as U64int
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64laws.bend as U64laws
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/u64laws.bend as U64laws
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64mont.bend as U64mont
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/u64mont.bend as U64mont
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as W64add
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64add.bend as W64add
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64clz.bend as W64clz
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64clz.bend as W64clz
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64div.bend as W64div
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64div.bend as W64div
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dm.bend as W64dm
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.bend as W64dm
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dmrem.bend as W64dmrem
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dmrem.bend as W64dmrem
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dmtop.bend as W64dmtop
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dmtop.bend as W64dmtop
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64est.bend as W64est
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64est.bend as W64est
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64isq.bend as W64isq
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64isq.bend as W64isq
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64m128.bend as W64m128
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64m128.bend as W64m128
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mm.bend as W64mm
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64mm.bend as W64mm
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mmtop.bend as W64mmtop
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64mmtop.bend as W64mmtop
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64mul
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64mul.bend as W64mul
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as W64sh
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64sh.bend as W64sh
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64sqrt
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64sqrt.bend as W64sqrt
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as Width
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/width.bend as Width
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as U64
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/u64/u64.bend as U64
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as U64div
import 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/u64/u64div.bend as U64div
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as Common
import 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bend as Common
import bend-collections-laws-math@1.0.0.0/spec/lib/numeric.bend as Numeric
import 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/numeric.bend as Numeric
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as F64
import 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.bend as F64
import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as Fixed
import 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.bend as Fixed
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as Generic
import 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.bend as Generic
import bend-collections-laws-math@1.0.0.0/spec/math/hash.bend as Hash
import 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/hash.bend as Hash
import bend-collections-laws-math@1.0.0.0/spec/math/instances.bend as Instances
import 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.bend as Instances
import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as Natural
import 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.bend as Natural
import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as Number
import 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.bend as Number
import bend-collections-laws-math@1.0.0.0/spec/math/pow2.bend as Pow2
import 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/pow2.bend as Pow2
import bend-collections-laws-math@1.0.0.0/spec/math/random.bend as Random
import 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.bend as Random
import bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend as Chacha8rand
import 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/chacha8rand.bend as Chacha8rand
import bend-collections-laws-math@1.0.0.0/spec/math/random/pcg.bend as Pcg
import 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/pcg.bend as Pcg
import bend-collections-laws-math@1.0.0.0/spec/math/random/rand.bend as Rand
import 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.bend as Rand
import bend-collections-laws-math@1.0.0.0/spec/math/random/source.bend as Source
import 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/source.bend as Source
import bend-collections-laws-math@1.0.0.0/spec/math/u64.bend as U64
import 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/u64.bend as U64
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as W64
import 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.bend as W64
import bend-collections-laws-math@1.0.0.0/src/containers/deque.bend as Deque
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/containers/deque.bend as Deque
import bend-collections-laws-math@1.0.0.0/src/containers/hash_table.bend as Hash_table
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/containers/hash_table.bend as Hash_table
import bend-collections-laws-math@1.0.0.0/src/containers/types/deque.bend as Deque
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/containers/types/deque.bend as Deque
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F64
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.bend as F64
import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as Fixed
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.bend as Fixed
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as Generic
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.bend as Generic
import bend-collections-laws-math@1.0.0.0/src/math/hash.bend as Hash
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/hash.bend as Hash
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as Instances
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.bend as Instances
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as Natural
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bend as Natural
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as Num
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.bend as Num
import bend-collections-laws-math@1.0.0.0/src/math/number.bend as Number
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.bend as Number
import bend-collections-laws-math@1.0.0.0/src/math/pow2.bend as Pow2
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/pow2.bend as Pow2
import bend-collections-laws-math@1.0.0.0/src/math/random/chacha8.bend as Chacha8
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8.bend as Chacha8
import bend-collections-laws-math@1.0.0.0/src/math/random/chacha8/block.bend as Block
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.bend as Block
import bend-collections-laws-math@1.0.0.0/src/math/random/pcg.bend as Pcg
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/pcg.bend as Pcg
import bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend as Rand
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.bend as Rand
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as U64
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.bend as U64
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as W64
import 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.bend as W64

Modules

• laws_math.bend 0 declarations
• proofs/lib/arith.bend 22 declarations
• proofs/lib/lemmas/proofs/addition.bend 9 declarations, 6 laws
• proofs/lib/lemmas/proofs/addition_bounds.bend 3 declarations
• proofs/lib/lemmas/proofs/counter.bend 4 declarations, 3 laws
• proofs/lib/lemmas/proofs/division_bounds.bend 5 declarations
• proofs/lib/lemmas/proofs/division_candidate.bend 5 declarations
• proofs/lib/lemmas/proofs/division_candidate_bound.bend 4 declarations
• proofs/lib/lemmas/proofs/division_invariant.bend 6 declarations
• proofs/lib/lemmas/proofs/division_no_overflow.bend 11 declarations
• proofs/lib/lemmas/proofs/division_quotient.bend 12 declarations
• proofs/lib/lemmas/proofs/division_remainder.bend 4 declarations
• proofs/lib/lemmas/proofs/division_shift.bend 7 declarations
• proofs/lib/lemmas/proofs/division_value.bend 10 declarations
• proofs/lib/lemmas/proofs/invariants.bend 17 declarations, 3 laws
• proofs/lib/lemmas/proofs/map_bridge.bend 26 declarations, 18 laws
• proofs/lib/lemmas/proofs/map_difference_order.bend 10 declarations, 9 laws
• proofs/lib/lemmas/proofs/map_index.bend 9 declarations, 8 laws
• proofs/lib/lemmas/proofs/map_insert.bend 35 declarations, 30 laws
• proofs/lib/lemmas/proofs/map_lookup.bend 13 declarations, 10 laws
• proofs/lib/lemmas/proofs/map_routing.bend 18 declarations, 13 laws
• proofs/lib/lemmas/proofs/modular_addition.bend 13 declarations
• proofs/lib/lemmas/proofs/modular_negation.bend 6 declarations
• proofs/lib/lemmas/proofs/nat_algebra.bend 16 declarations
• proofs/lib/lemmas/proofs/native_map.bend 49 declarations, 44 laws
• proofs/lib/lemmas/proofs/natural_division.bend 6 declarations
• proofs/lib/lemmas/proofs/natural_products.bend 8 declarations
• proofs/lib/lemmas/proofs/negation_magnitude.bend 5 declarations
• proofs/lib/lemmas/proofs/numeric.bend 24 declarations, 23 laws
• proofs/lib/lemmas/proofs/string_compare.bend 21 declarations, 18 laws
• proofs/lib/lemmas/proofs/subtraction_bounds.bend 7 declarations
• proofs/lib/lemmas/proofs/word_addition.bend 3 declarations
• proofs/lib/lemmas/proofs/word_bounds.bend 2 declarations, 2 laws
• proofs/lib/lemmas/proofs/word_comparison.bend 5 declarations
• proofs/lib/lemmas/proofs/word_multiplication.bend 9 declarations
• proofs/lib/lemmas/proofs/word_shift.bend 6 declarations
• proofs/lib/lemmas/proofs/word_subtraction.bend 5 declarations
• proofs/lib/lemmas/proofs/word_value.bend 19 declarations
• proofs/lib/lemmas/spec/numeric.bend 17 declarations
• proofs/lib/lemmas/spec/unsigned_division.bend 1 declarations
• proofs/lib/lemmas/src/cache.bend 60 declarations, 1 laws
• proofs/lib/lemmas/src/time.bend 8 declarations
• proofs/lib/lemmas/src/wide.bend 27 declarations
• proofs/lib/lemmas/types/model.bend 12 declarations
• proofs/lib/list.bend 46 declarations
• proofs/lib/logic.bend 24 declarations
• proofs/lib/nat.bend 75 declarations
• proofs/lib/two_list.bend 7 declarations
• proofs/lib/u32.bend 43 declarations
• proofs/lib/u32alg.bend 36 declarations
• proofs/lib/u32div.bend 28 declarations
• proofs/lib/u32half.bend 15 declarations
• proofs/lib/word.bend 41 declarations
• proofs/lib/words32.bend 13 declarations
• proofs/math/hash/hash.bend 8 declarations
• proofs/math/natural/arith.bend 23 declarations
• proofs/math/natural/bits.bend 14 declarations
• proofs/math/natural/fact.bend 28 declarations
• proofs/math/natural/gcd.bend 18 declarations
• proofs/math/natural/inverse.bend 25 declarations
• proofs/math/natural/lcm.bend 22 declarations
• proofs/math/natural/lists.bend 24 declarations
• proofs/math/natural/logs.bend 17 declarations
• proofs/math/natural/misc.bend 14 declarations
• proofs/math/natural/modpow.bend 8 declarations
• proofs/math/natural/proof.bend 54 declarations
• proofs/math/natural/roots.bend 29 declarations
• proofs/math/natural/sqrtn.bend 13 declarations
• proofs/math/number/bitcount.bend 4 declarations
• proofs/math/number/egcd.bend 13 declarations
• proofs/math/number/fixprime.bend 23 declarations
• proofs/math/number/prime.bend 22 declarations
• proofs/math/number/proof.bend 77 declarations
• proofs/math/pow2/pow2.bend 2 declarations
• proofs/math/proof.bend 13 declarations
• proofs/math/random/below.bend 15 declarations
• proofs/math/random/bits.bend 9 declarations
• proofs/math/random/bounded.bend 3 declarations
• proofs/math/random/chacha8/block.bend 5 declarations
• proofs/math/random/chacha8/rounds.bend 6 declarations — Generated by tools/generators/chacha8rand_gen.py; do not edit.
• proofs/math/random/chacha8/seed.bend 4 declarations
• proofs/math/random/chacha8/stream.bend 7 declarations
• proofs/math/random/float.bend 48 declarations
• proofs/math/random/fround.bend 44 declarations
• proofs/math/random/lemire.bend 57 declarations
• proofs/math/random/pcg/impl.bend 8 declarations
• proofs/math/random/pcg/step.bend 12 declarations
• proofs/math/random/pcg/xor.bend 9 declarations
• proofs/math/random/proof.bend 5 declarations
• proofs/math/random/proof_draws.bend 8 declarations
• proofs/math/random/proof_float.bend 2 declarations
• proofs/math/random/proof_pcg.bend 12 declarations
• proofs/math/random/shuffle.bend 18 declarations
• proofs/math/random/uint64n.bend 41 declarations
• proofs/math/random/wrappers.bend 32 declarations
• proofs/math/typed/bgcdnat.bend 78 declarations
• proofs/math/typed/combnat.bend 26 declarations
• proofs/math/typed/examples.bend 56 declarations
• proofs/math/typed/f64adda.bend 15 declarations
• proofs/math/typed/f64addb.bend 9 declarations
• proofs/math/typed/f64addc.bend 14 declarations
• proofs/math/typed/f64adde.bend 3 declarations
• proofs/math/typed/f64addf.bend 24 declarations
• proofs/math/typed/f64addg.bend 21 declarations
• proofs/math/typed/f64addh.bend 4 declarations
• proofs/math/typed/f64addp.bend 9 declarations
• proofs/math/typed/f64adds.bend 9 declarations
• proofs/math/typed/f64addv.bend 14 declarations
• proofs/math/typed/f64bits.bend 45 declarations
• proofs/math/typed/f64bl.bend 9 declarations
• proofs/math/typed/f64close.bend 14 declarations
• proofs/math/typed/f64cmp.bend 39 declarations
• proofs/math/typed/f64conv.bend 30 declarations
• proofs/math/typed/f64divc.bend 27 declarations
• proofs/math/typed/f64divd.bend 5 declarations
• proofs/math/typed/f64divf.bend 8 declarations
• proofs/math/typed/f64divn.bend 22 declarations
• proofs/math/typed/f64divq.bend 10 declarations
• proofs/math/typed/f64divv.bend 15 declarations
• proofs/math/typed/f64divx.bend 2 declarations
• proofs/math/typed/f64exp.bend 23 declarations
• proofs/math/typed/f64fmod.bend 81 declarations
• proofs/math/typed/f64light.bend 21 declarations
• proofs/math/typed/f64mexp.bend 11 declarations
• proofs/math/typed/f64misc.bend 11 declarations
• proofs/math/typed/f64modf.bend 8 declarations
• proofs/math/typed/f64mul.bend 6 declarations
• proofs/math/typed/f64mulc.bend 14 declarations
• proofs/math/typed/f64mulf.bend 8 declarations
• proofs/math/typed/f64mulp.bend 9 declarations
• proofs/math/typed/f64mulv.bend 6 declarations
• proofs/math/typed/f64next.bend 42 declarations
• proofs/math/typed/f64norm.bend 14 declarations
• proofs/math/typed/f64nrp.bend 13 declarations
• proofs/math/typed/f64ofnat.bend 7 declarations
• proofs/math/typed/f64ratio.bend 13 declarations
• proofs/math/typed/f64rint.bend 27 declarations
• proofs/math/typed/f64round.bend 105 declarations
• proofs/math/typed/f64rtools.bend 22 declarations
• proofs/math/typed/f64sqa.bend 27 declarations
• proofs/math/typed/f64sqc.bend 31 declarations
• proofs/math/typed/f64sqf.bend 3 declarations
• proofs/math/typed/f64sqk.bend 8 declarations
• proofs/math/typed/f64sqn.bend 9 declarations
• proofs/math/typed/f64sqr.bend 54 declarations
• proofs/math/typed/f64sqs.bend 9 declarations
• proofs/math/typed/f64sqv.bend 39 declarations
• proofs/math/typed/f64sqw.bend 3 declarations
• proofs/math/typed/f64sqx.bend 1 declarations
• proofs/math/typed/f64tools.bend 28 declarations
• proofs/math/typed/fix32.bend 63 declarations
• proofs/math/typed/fix64.bend 61 declarations
• proofs/math/typed/fixbits.bend 11 declarations
• proofs/math/typed/fixbytes.bend 60 declarations
• proofs/math/typed/fixgen.bend 16 declarations
• proofs/math/typed/float.bend 41 declarations
• proofs/math/typed/montnat.bend 11 declarations
• proofs/math/typed/natcmp.bend 21 declarations
• proofs/math/typed/natfuel.bend 68 declarations
• proofs/math/typed/natlight.bend 5 declarations
• proofs/math/typed/shrn.bend 12 declarations
• proofs/math/typed/u32.bend 23 declarations
• proofs/math/typed/u32int.bend 147 declarations
• proofs/math/typed/u32laws.bend 45 declarations
• proofs/math/typed/u32mont.bend 35 declarations
• proofs/math/typed/u64bgcd.bend 40 declarations
• proofs/math/typed/u64int.bend 147 declarations
• proofs/math/typed/u64laws.bend 26 declarations
• proofs/math/typed/u64mont.bend 51 declarations
• proofs/math/typed/w64add.bend 51 declarations
• proofs/math/typed/w64clz.bend 34 declarations
• proofs/math/typed/w64div.bend 26 declarations
• proofs/math/typed/w64dm.bend 30 declarations
• proofs/math/typed/w64dmrem.bend 10 declarations
• proofs/math/typed/w64dmtop.bend 8 declarations
• proofs/math/typed/w64est.bend 26 declarations
• proofs/math/typed/w64isq.bend 21 declarations
• proofs/math/typed/w64m128.bend 16 declarations
• proofs/math/typed/w64mm.bend 11 declarations
• proofs/math/typed/w64mmtop.bend 8 declarations
• proofs/math/typed/w64mul.bend 42 declarations
• proofs/math/typed/w64sh.bend 47 declarations
• proofs/math/typed/w64sqrt.bend 36 declarations
• proofs/math/typed/width.bend 60 declarations
• proofs/math/u64/u64.bend 31 declarations
• proofs/math/u64/u64div.bend 39 declarations
• spec/lib/common.bend 21 declarations
• spec/lib/numeric.bend 15 declarations
• spec/math/f64.bend 125 declarations
• spec/math/fixed.bend 50 declarations
• spec/math/generic.bend 50 declarations
• spec/math/hash.bend 2 declarations
• spec/math/instances.bend 17 declarations
• spec/math/natural.bend 58 declarations
• spec/math/number.bend 10 declarations
• spec/math/pow2.bend 1 declarations
• spec/math/random.bend 23 declarations
• spec/math/random/chacha8rand.bend 32 declarations
• spec/math/random/pcg.bend 6 declarations
• spec/math/random/rand.bend 12 declarations
• spec/math/random/source.bend 3 declarations
• spec/math/u64.bend 9 declarations
• spec/math/w64.bend 27 declarations
• src/containers/deque.bend 32 declarations
• src/containers/hash_table.bend 120 declarations
• src/containers/types/deque.bend 16 declarations
• src/math/f64.bend 228 declarations
• src/math/fixed.bend 85 declarations
• src/math/generic.bend 98 declarations
• src/math/hash.bend 4 declarations
• src/math/instances.bend 11 declarations
• src/math/natural.bend 52 declarations
• src/math/num.bend 30 declarations
• src/math/number.bend 9 declarations
• src/math/pow2.bend 2 declarations
• src/math/random/chacha8.bend 20 declarations
• src/math/random/chacha8/block.bend 10 declarations — Generated by tools/generators/chacha8rand_gen.py; do not edit.
• src/math/random/pcg.bend 17 declarations
• src/math/random/rand.bend 53 declarations
• src/math/u64.bend 19 declarations
• src/math/w64.bend 131 declarations

Other files

• LICENSE 1,101 bytes

Dependencies

No imports from other hub packages.

Dependents

• 0x993b989c via laws.bend: import bend-collections-laws-math@1.0.0.0/laws_math.bend as Math

Status on bend 2.0.36