Coq Notes

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.