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 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50
/*! # Voile Util This is a crate extracted from the codebase of the [Voile] type checker to help the development of other dependently-typed lambda calculus type checkers. It contains helper functions for the [Pest] parser (supported via optional feature `parser`), a non-empty vector, some location utils, a unique-ID type with utils, many indices type support (meta-variable indices, global definition indices, de-bruijn indices) with pattern matcher and operators, a lisp parser for term generation, and universe level utilities (with omega). All dependencies are optional, thus very lightweight. [Voile]: https://docs.rs/voile [Pest]: https://pest.rs */ /// Syntactical information. pub mod loc; /// Unique-ID utilities. #[macro_use] pub mod uid; /// Defines the `Axiom` type and some functions on it. pub mod axiom; /// `Level`-related definitions and relevant operations and traits. pub mod level; /// Helper functions for pest. #[cfg(feature = "parser")] #[macro_use] pub mod pest_util; /// A Lisp parser as some testing utility. #[cfg(feature = "lisp")] pub mod lisp; /// Not using the [vec1 crate](https://docs.rs/vec1/1.4.0) because it doesn't have `fold1`. pub mod vec1; /// Generic meta variable utilities. pub mod meta; /// `VarRec`, `PiSig`, etc. pub mod tags;