mortberg / cubicaltt

Experimental implementation of Cubical Type Theory
https://arxiv.org/abs/1611.02108
MIT License
571 stars 76 forks source link

List reserved names #37

Closed abooij closed 8 years ago

abooij commented 8 years ago

As a (relative) newcomer to cubicaltt, at times I found the example code somewhat difficult to grasp because it seemed to be using all kinds of previously undefined terms such as "transport" and "glue". I believe it would help accessibility of cubicaltt if the reserved names of the syntax are listed somewhere (e.g. in the readme), so that users do not need to refer to Exp.cf, and will not run into weird bugs when they define a "glue" constructor for their favorite HIT.

mortberg commented 8 years ago

I added this to the README now.