15 releases

0.2.2 Dec 1, 2019
0.2.1 Nov 26, 2019
0.2.0 Oct 23, 2019
0.1.11 Oct 13, 2019
0.1.5 Sep 21, 2019

#1273 in Development tools


Used in 2 crates

Apache-2.0

31KB
769 lines

Voile's utilities

Crates.io Crates.io Crates.io docs.rs

This is a crate extracted from Voile 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 type as the maximum universe).


lib.rs:

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.

Dependencies

~0–560KB
~11K SLoC