~/jendhub

laws_math.bend

bend-collections-laws-math@1.0.0.0 · 24 lines · 0 definitions

1import Base
2
3# bend-collections-laws-math: the proved laws of bend-collections' math: integer math, per-type math, software binary64, 64-bit words, number theory.
4# Importing this file checks every proof root below; see docs/*_CONTRACTS.md
5# for what each clause states and what is not proved. Part of
6# bend-collections-laws (laws.bend imports all three parts by name).
7
8import bend-collections-laws-math@1.0.0.0/proofs/math/number/proof.bend as MathNumberProof
9import bend-collections-laws-math@1.0.0.0/proofs/math/proof.bend as MathProof
10import bend-collections-laws-math@1.0.0.0/proofs/math/random/proof.bend as MathRandomProof
11import bend-collections-laws-math@1.0.0.0/proofs/math/random/proof_draws.bend as MathRandomProofDraws
12import bend-collections-laws-math@1.0.0.0/proofs/math/random/proof_float.bend as MathRandomProofFloat
13import bend-collections-laws-math@1.0.0.0/proofs/math/random/proof_pcg.bend as MathRandomProofPcg
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/examples.bend as MathTypedExamples
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64close.bend as MathTypedF64close
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divc.bend as MathTypedF64divc
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend as MathTypedF64fmod
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64misc.bend as MathTypedF64misc
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64modf.bend as MathTypedF64modf
20import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend as MathTypedF64next
21import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64ofnat.bend as MathTypedF64ofnat
22import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64ratio.bend as MathTypedF64ratio
23import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend as MathTypedF64sqc
24import bend-collections-laws-math@1.0.0.0/proofs/math/typed/float.bend as MathTypedFloat