Project-PL12

$\lambda_{\Pi}^{+}$-calculus, with implicit arguments/holes and some useful extensions over LambdaPi.

Currently, this calculus uses The True McBride Universe Type in Type (* : *) which is known for its inconsistency. We're actively considering alternatives, such as impredicative proposition types, universe hierarchies and universe polymorphism.