Crate voile_util

Source
Expand description

§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§