coqdependent-typetheorem-proving

Programming in the Calculus of Inductive Constructions with Coq

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?

Solution

  • If you want no syntactic sugar at all you should do Set Printing All.