pocket_prover-set
A base logical system for PocketProver to reason about set properties
extern crate pocket_prover;
extern crate pocket_prover_set;
use *;
use *;
There are 4 bits of information, used to derive all other properties:
any
- All types, including those not defineduniq
- A unique valuefin_many
- Many but finite number of valuesinf_many
- Many but infinite number of values
A set is empty (.none()
) when all bits are set to 0.
A set is non-empty (.some()
) when at least bit is set to 1.
A set is undefined when it is any
but neither unique, finite or infinite.
Here is an example of a proof of 8 sets:
extern crate pocket_prover;
extern crate pocket_prover_set;
use *;
use *;