The Coq mailing list

["Manny Romero" <mannyromero AT mail.com>]

Hello! Apologies if this isn't the appropriate mailing list; I couldn't find a Coq beginners' list anywhere.

 

I am someone who is ignorant of the most basic aspects of computers who is getting started with Coq. I have installed the CoqIde 8.4pl4 on Linux Mint 18 and used it successfully with some simple tutorials.

 

Now, however, I am trying to use the textbook **Adam Chlipala** ( http://adam.chlipala.net/cpdt/ ); and, as explained at the beginning of Chapter 2, it requires me to "Require Import" various files to follow along with the texts and do the exercises. Specifically, I must:

 

Require Import Bool Arith List Cpdt.CpdtTactics.
Set Implicit Arguments.
Set Asymmetric Patterns.

 

Cpdt.CpdtTactics is among the files available for download on the Chlipala website. I downloaded all the files and "unzipped" them into a subfolder I made within my folder /home/mannyromero/Downloads; but that is not among the locations I see when I enter "Print LoadPath" into the CoqIde, which I assume is why I get a message "Error: Cannot find library Cpdt.CpdtTactics in loadpath" when I try to Require Import as above.

 

What do I do to add the location of the Cpdt.CpdtTactics file to the CoqIde's list somehow so that I can Require Import it and proceed with the textbook exercises?

 

Or, if this is off topic or inappropriate, apologies and can someone direct me to a better community to ask this question?