prop 0.47.0

Propositional logic with types in Rust
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

/*

Demonstrates normalisation of coordinates.

Normalisation happens after coordinates are transformed.

*/

use prop::*;
use path_semantics::*;
use nat::*;

// Normalise corners from `2 1 2 0` to `0 1 2 2`.
pub fn proof<A: LProp<N = Zero>, B: LProp<N = One>, C: LProp<N = Two>, D: LProp<N = Two>>()
-> PSemNaive<A, B, C, D> {
    assume_norm_path_level::<C, B, D, A>()
}

fn main() {}