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, 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.

Modules

axiom	Defines the Axiom type and some functions on it.
level	Level-related definitions and relevant operations and traits.
lisp	A Lisp parser as some testing utility.
loc	Syntactical information.
meta	Generic meta variable utilities.
pest_util	Helper functions for pest.
tags	VarRec, PiSig, etc.
uid	Unique-ID utilities.
vec1	Not using the vec1 crate because it doesn't have fold1.

Macros

many_prefix_parser
next_rule
tik_tok
uid_basic_operations_impl