The Coq mailing list

[karsar <karen.sarkisyan AT gmail.com>]

You'll need to read "1.6.3 Installation and Emacs Set-Up" from Chapter 1 (Introduction) in Cpdt book and do all the steps beyond unzipping.

There is an easy way to experiment with code in your browser as well.

At https://x80.org/collacoq/ you need to click on Packages (right and down at the page) 

to load required packages, like cpdt, cor-arith, coq-base...

Then, to import all you need, just do:

From Coq Require Import Bool.Bool Arith.Arith Lists.List. 

From Cpdt Require Import CpdtTactics.

Set Implicit Arguments.
Set Asymmetric Patterns.

Hope this is useful. 

Best,

Karen Sargsyan

On Sun, Aug 20, 2017 at 1:43 PM, Manny Romero <mannyromero AT mail.com> wrote:

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?