Coq Notes

Originally written: October 19th, 2020

Notes to self while learning to use Coq, the proof assistant language.

  • Use Set Printing All to remove the syntactic sugar. However this can potentially make things horribly difficult to read, so beware.

  • Compiling with coq_make_file and make may fail and trying to import may give you a directory missing error:
                      Error: Unable to locate library yourFileToImport.
                      Makefile:270: recipe for target 'yourCurrentFileThatImports.vo' failed
    In that case, compile explicitly with coqc -Q . LF yourFileToImport.v in the command line and then when importing, do Require Export LF.yourFileToImport.