karpal-proof 0.6.1

Algebraic law witnesses and refinement types for the Industrial Algebra ecosystem
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

# karpal-proof

Algebraic law witnesses, rewrite evidence, and refinement types for the Karpal ecosystem.

`karpal-proof` provides the in-Rust proof layer used by Karpal:

- `Proven<P, T>` for values paired with evidence markers
- property markers for algebraic laws
- `Rewrite` witnesses for equational reasoning
- refinement types such as `NonEmpty<T>` and `Positive<T>`
- optional derive-macro integration via `karpal-proof-derive`

## Features

- `std` *(default)*
- `alloc`
- `derive` *(default)*

## Example

```rust
use karpal_proof::{IsAssociative, Proven};

let value = unsafe { Proven::<IsAssociative, i32>::axiom(42) };
assert_eq!(*value, 42);
```

See the workspace `README.md` and `docs/reference/proof-verification.html` for the broader proof and external verification story.

## License

Apache-2.0