The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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