An exploration of the power and Turing-completeness of Rust's type system. Leverages the language's polymorphism (generics) and the resultant unification (trait solving) to automatically prove various facts about set theory from axioms. This repository mostly focuses on implementing a set-theoretic definition of the natural numbers. Compiler-checked 'proofs' are found in src/tests.rs.
-
Notifications
You must be signed in to change notification settings - Fork 0
Codadillo/type-level-set-theory
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
No description, website, or topics provided.
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published