Crate pocket_prover_set [−] [src]
pocket_prover-set
A base logical system for PocketProver to reason about set properties
extern crate pocket_prover; extern crate pocket_prover_set; use pocket_prover::*; use pocket_prover_set::*; fn main() { println!("Result {}", Set::imply( |s| s.fin_many, |s| not(s.inf_many) )); }
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 pocket_prover::*; use pocket_prover_set::*; fn main() { println!("Result {}", Set8::imply( |sets| and(sets.uniqs(|xs| xorn(xs)), sets.a.uniq), |sets| not(sets.h.uniq) )); }
Structs
Set |
Conditions that holds for a set in general. |
Set2 |
Contains 2 sets. |
Set3 |
Contains 3 sets. |
Set4 |
Contains 4 sets. |
Set5 |
Contains 5 sets. |
Set6 |
Contains 6 sets. |
Set7 |
Contains 7 sets. |
Set8 |
Contains 8 sets. |