mortberg / cubicaltt

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

Allow opaque/transparent in the command line #89

Open guillaumebrunerie opened 7 years ago

guillaumebrunerie commented 7 years ago

It would be nice to be allowed to write > opaque f or > transparent f at the command line, rather than having to write it in the file and reload all of it.