[−][src]Crate pocket_prover_set
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 6 sets:
extern crate pocket_prover; extern crate pocket_prover_set; use pocket_prover::*; use pocket_prover_set::*; fn main() { println!("Result {}", <(Set, Set, Set, Set, Set, Set)>::imply( |sets| and(sets.uniqs(|xs| xorn(xs)), sets.0.uniq), |sets| not(sets.5.uniq) )); }
Structs
Set | Conditions that holds for a set in general. |
Traits
MSet | Implemented on tuples of sets to access arrays of same kind of bits. |