The Coq mailing list

[Ismael Figueroa <ifigueroap AT gmail.com>]

Thanks Michael and Beta, indeed that was the issue.

As Beta pointed out, I found this situation when I started working on Software Foundations. It appears that the online version does not show the second definition of admit, which is indeed in the .v file.

Best regards,

2015-02-25 10:46 GMT-03:00 Beta Ziliani <beta AT mpi-sws.org>:

I should point out that in Software Foundations there's a definition called "admit", which can be confused with the tactic. Its definition is:

Definition admit {T: Type} : T.  Admitted.

Written from mobile. Excuse my limited communication.

On Feb 25, 2015 10:04 AM, "Soegtrop, Michael" <michael.soegtrop AT intel.com> wrote:

Dear Ismael,

 

“admit” is a tactic – part of the Ltac language, but Definition expects a Gallina term after the :=. In the Gallina world, admit is undefined.

 

This does work:

 

Definition foo (a:nat) (b:nat): nat. admit. Defined.

 

Definition foo (a:nat) (b:nat): nat. Admitted.

 

Closing the Definition with a . before a := enters proof mode, and Ltac is expected.

 

In the 8.5 beta you can also use the syntax $( tactic )$ where a Gallina term is expected like this:

 

Definition foo (a:nat) (b:nat): nat := $( admit )$.

 

but this doesn’t work in 8.4pl5.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Ismael Figueroa
Sent: Tuesday, February 24, 2015 4:18 PM
To: coq-club AT inria.fr
Subject: [Coq-Club] Weird installation error in OS X Mavericks

 

Hi club,

 

Apologies if this is not the right venue for this kind of questions

 

I installed Coq 8.4pl5 using Homebrew (brew install coq), but for some reason I cannot use the admit tactic. As far as I understand, admit is now built-in in Coq. I asked a colleague to check if it was available and indeed it was working on his machine, hence I assume it is some weird installation issue... Can anyone please point me to where is the issue happening?

 

I attach a small file with my interaction with coqtop and the actual error message.

 

Thanks

 

--

Ismael

--

Ismael