英文:
Programming in the Calculus of Inductive Constructions with Coq
问题
有时候我想编写接近裸骨CIC（归纳构造演算）的程序，以更好地理解内部运作。
然后，我需要自定义一些设置来更改Coq环境的默认行为，比如Set Printing Implicit。
还有其他我可以做的吗？
英文:
Sometimes I want to write programs close to bare-bone CIC (Calculus of Inductive Constructions) to get a better grasp of the internal workings.
I then need to customize some settings to change the default behavior of the Coq environment, such as Set Printing Implicit.
Are there more that I can do?
答案1
得分: 2
如果你完全不想使用任何语法糖，你应该执行 Set Printing All。
英文:
If you want no syntactic sugar at all you should do Set Printing All.
答案2
得分: 1
你可以使用-noinit选项启动Coq，这将避免加载Prelude，因此只要你不使用符号表示法，你就接近了裸的CIC演算，但截止到今天，没有办法禁用类型推断。
英文:
You can launch coq with the -noinit option, that will avoid loading the Prelude, so as long as you don't use notations, you are pretty close to the bare CIC calculus, but as of today there is not way to disable type-inference.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论