Crate junglefowl

Brutally murdering Rust’s type system one proof at a time.

Re-exports

• pub use nest::Nest;

Modules

• nest
  Compile-time-length arrays that can be spliced up however you’d like while keeping full knowledge of every piece’s length.
• peano
  Peano arithmetic: essentially unary encoding in types rather than values.

Macros

• add
  Add two Peano types.
• array
  Array type holding N elements of type T.
• nest
  Place N elements into a nested tuple of known shape at compile time. Inspired by frunk’s implementation but with trailing comma support and a different sentinel node.
• peano
  Create a unique type representing the given number.
• split
  Syntactic sugar for Split::<peano!($n)>>::split($nest).
• static_assert_eq
  Assert at compile time that two Peano types represent the same number.
• static_assert_ne
  Assert at compile time that two Peano types represent different numbers.
• static_assert_nonzero
  Assert at compile time that a Peano type does not represent zero (and thus must be positive).
• static_assert_zero
  Assert at compile time that a Peano type represents zero.
• sub
  Subtract two Peano types.

Enums

• False
  A type that can never be instantiated (inhabited by zero values). Corresponds to a false statement under the Curry-Howard correspondence.