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