Constructive User Interface for Constructive Mathematics

Starting today, it's possible to develop dependent type theories succinctly through a user interface that provides instant feedback and prevents brain farting in context.

To try it out, checkout the wip branch, make sure you have glib and ncurses, compile with autotools, and run the generated "v" executable.

It's not yet possible to perform derivations, but we are working on it. Stay tuned!