Papuq: a Coq assistant ?
Jacek Chrza̧szcz, Jakub Sakowicz · 2007
We describe an extension to CoqIDE called Papuq, targeted at students learning the basics of mathematical reasoning. The extension tries to bridge the gap between natural language used to teach proofs during the university course and the artificial language of Coq proofs. We believe it will give the students the possibility to practice writing proofs by themselves and at the same time to learn writing precise proofs in natural language.