Crate karpal_proof 

Re-exports

pub use proven::Proven;

pub use rewrite::Justifies;

pub use rewrite::Rewrite;

pub use refinement::NonEmpty;

pub use refinement::Positive;

pub use property::*;

Modules

law_check

Runtime law-checking helpers.

property

proven

refinement

rewrite

Derive Macros

VerifyCommutative

Re-export derive macros when the derive feature is enabled. Derive VerifyCommutative: generates proptest for commutativity of combine.

VerifyGroup

Re-export derive macros when the derive feature is enabled. Derive VerifyGroup: generates proptest for left/right inverse.

VerifyLattice

Re-export derive macros when the derive feature is enabled. Derive VerifyLattice: generates proptests for associativity, commutativity, idempotency, and absorption of meet/join.

VerifyMonoid

Re-export derive macros when the derive feature is enabled. Derive VerifyMonoid: generates proptest for left/right identity of empty.

VerifyRing

Re-export derive macros when the derive feature is enabled. Derive VerifyRing: generates proptest for additive inverse (negate).

VerifySemigroup

Re-export derive macros when the derive feature is enabled. Derive VerifySemigroup: generates proptest for associativity of combine.

VerifySemiring

Re-export derive macros when the derive feature is enabled. Derive VerifySemiring: generates proptests for additive monoid, multiplicative monoid, distributivity, and zero annihilation.