1	import Base
2	
3	# bend-collections-laws: every proved clause of bend-collections, in one entry.
4	#
5	# The laws are published in three parts (BendHub caps a package at 16 MiB);
6	# importing this file imports all three, which checks every proof root of the
7	# library: the containers' SPARK-style contracts, the math contracts, and the
8	# crypto and random refinements (each implementation equal to its standard's
9	# executable specification, for every input). Import one part, or one
10	# package's root inside it, when you need only those laws, e.g.
11	#
12	#   import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend as AeadLaws
13	#
14	# What is and is not proved is listed in docs/*_CONTRACTS.md.
15	
16	import bend-collections-laws-containers@1.0.0.0/laws_containers.bend as Containers
17	import bend-collections-laws-math@1.0.0.0/laws_math.bend as Math
18	import bend-collections-laws-crypto@1.0.0.0/laws_crypto.bend as Crypto