1	import 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	
8	import ./proofs/math/number/proof.bend as MathNumberProof
9	import ./proofs/math/proof.bend as MathProof
10	import ./proofs/math/random/proof.bend as MathRandomProof
11	import ./proofs/math/random/proof_draws.bend as MathRandomProofDraws
12	import ./proofs/math/random/proof_float.bend as MathRandomProofFloat
13	import ./proofs/math/random/proof_pcg.bend as MathRandomProofPcg
14	import ./proofs/math/typed/examples.bend as MathTypedExamples
15	import ./proofs/math/typed/f64close.bend as MathTypedF64close
16	import ./proofs/math/typed/f64divc.bend as MathTypedF64divc
17	import ./proofs/math/typed/f64fmod.bend as MathTypedF64fmod
18	import ./proofs/math/typed/f64misc.bend as MathTypedF64misc
19	import ./proofs/math/typed/f64modf.bend as MathTypedF64modf
20	import ./proofs/math/typed/f64next.bend as MathTypedF64next
21	import ./proofs/math/typed/f64ofnat.bend as MathTypedF64ofnat
22	import ./proofs/math/typed/f64ratio.bend as MathTypedF64ratio
23	import ./proofs/math/typed/f64sqc.bend as MathTypedF64sqc
24	import ./proofs/math/typed/float.bend as MathTypedFloat