A small and experimental Rust library with a type-level representation of booleans with companion connectives for compile-time sort-of fun with logic.
```rust
type Tollens >; fn whatisreality The intuition behind it is as follows: Consider the trait Notice the lack of associated functions, it only has an associated type. And the implementation of ```rust
struct True;
struct False; impl Negation for True {
type Output = False
} impl Negation for False {
type Output = True
}
``` We may treat A function with more inputs would correspond to a trait with generic parameters, such as Where we would now need four RusTollens builds on top of these ideas to compute simple logical statements at the type-level, statically at compile-time. Fairly likely not an amazingly applicable library, still the idea of encoding invariants at type-level such that the compiler can verify on our behalf them is incredibly powerful. Therefore, this small experiment aims to give some more food for thought and invite the reader to explore and appreciate Rust's type-system to its maximum.>, Not
Negation:rust
trait Negation {
type Output;
}
Negation for the types True and False:Negation as a piece-wise function from types to types, where Self would be the input and Output the output, each combination of input types gives rise to a function (impl). In pseudo-code:
negation(True) = False
negation(False) = True
Conjunction defined below:rust
trait Conjunction<L> {
type Output;
}
impls to exhaust the four combinations of True and False, for instance:rust
impl Conjunction<True> for False {
// False AND True IS False
type Output = False;
}