litex-lang 0.9.6-beta

A simple formal proof language and verifier, learnable in 2 hours
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40

mod verify_and_chain_fact;
mod verify_atomic_fact;
mod verify_atomic_fact_with_known_forall;
mod verify_by_syntax;
mod verify_equality;
mod verify_equality_by_builtin_rules;
mod verify_exist_fact;
mod verify_exist_fact_with_known_forall;
mod verify_fact;
mod verify_fact_well_defined;
mod verify_facts_the_same_type_and_return_matched_args;
mod verify_fn_set_equality_builtin_rule;
mod verify_forall_fact_forall_fact_with_iff;
mod verify_helper;
mod verify_builtin_rules;
mod verify_non_equational_atomic_fact;
pub(crate) use verify_builtin_rules::{compare_normalized_number_str_to_zero, NumberCompareResult};
mod verify_number_in_standard_set;
mod verify_obj_well_defined;
mod verify_or_fact;
mod verify_or_fact_with_known_forall;
mod verify_restrict_by_def;
mod verify_state;
mod verify_arg_satisfy_param_def;
mod verify_obj_satisfy_struct;
mod verify_obj_satisfy_family;

pub use verify_number_in_standard_set::number_is_in_n;
pub use verify_number_in_standard_set::number_is_in_n_pos;
pub use verify_number_in_standard_set::number_is_in_q_neg;
pub use verify_number_in_standard_set::number_is_in_q_nz;
pub use verify_number_in_standard_set::number_is_in_q_pos;
pub use verify_number_in_standard_set::number_is_in_r_neg;
pub use verify_number_in_standard_set::number_is_in_r_nz;
pub use verify_number_in_standard_set::number_is_in_r_pos;
pub use verify_number_in_standard_set::number_is_in_z;
pub use verify_number_in_standard_set::number_is_in_z_neg;
pub use verify_number_in_standard_set::number_is_in_z_nz;

pub use verify_state::VerifyState;