cubicaltt
cubicaltt copied to clipboard
mortberg
Experimental implementation of Cubical Type Theory
The error message for type checking errors, while correct, is rather unhelpful in bigger proofs. It would be nice if it could at least state a line number where things...
``` module test where import nat suc' : nat -> nat = suc ``` yields: ``` Type checking failed: expected a data type for the constructor suc but got Pi...
If those changes is suitable, I will submit the package to nixpkgs after merged. :)
