Crate voile_util

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, a lisp parser for term generation, and universe level utilities (with omega).

All dependencies are optional, thus very lightweight.

Modules

axiom	Defines the Axiom type and some functions on it.
level	Level-related definitions and relevant operations and traits.
loc	Syntactical information.
meta	Generic meta variable utilities.
tags	VarRec, PiSig, etc.
uid	Unique-ID utilities.
vec1	Not using https://docs.rs/vec1/1.4.0 because it doesn't have fold1.

Macros

uid_basic_operations_impl