I’ve just started using Coq, a proof assistant, – and a pretty cool one at that. But just like anything else, being new to Coq means I run into some silly problems sometimes (read: often). I’ll post those issues here in the hopes that some other newbie comes across it and doesn’t make my mistakes.
Here’s my setup at the moment:
- OSX 10.7.5
- CoqIde version 8.4
If you “Require Export Somelibrary” and you get this error, you may need to compile Somelibrary.
Error: Cannot find library Somelibrary in loadpath
Open Somelibrary into CoqIde and click Compile -> Compile Buffer.