Crates.io | pocket_prover-set |
lib.rs | pocket_prover-set |
version | 0.5.0 |
source | src |
created_at | 2018-02-23 11:06:07.215792 |
updated_at | 2022-10-07 21:47:16.557389 |
description | A base logical system for PocketProver to reason about set properties |
homepage | https://github.com/advancedresearch/pocket_prover-set |
repository | https://github.com/advancedresearch/pocket_prover-set.git |
max_upload_size | |
id | 52503 |
size | 19,088 |
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 valuesA 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 {}", <(Set, Set, Set, Set, Set, Set, Set, Set)>::imply(
|sets| and(sets.uniqs(|xs| xorn(xs)), sets.0.uniq),
|sets| not(sets.7.uniq)
));
}