voile_util/
lib.rs

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