coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] Weird installation error in OS X Mavericks
- Date: Wed, 25 Feb 2015 13:03:28 +0000
- Accept-language: de-DE, en-US
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
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 |
- [Coq-Club] Weird installation error in OS X Mavericks, Ismael Figueroa, 02/24/2015
- RE: [Coq-Club] Weird installation error in OS X Mavericks, Soegtrop, Michael, 02/25/2015
- RE: [Coq-Club] Weird installation error in OS X Mavericks, Beta Ziliani, 02/25/2015
- Re: [Coq-Club] Weird installation error in OS X Mavericks, Ismael Figueroa, 02/25/2015
- RE: [Coq-Club] Weird installation error in OS X Mavericks, Beta Ziliani, 02/25/2015
- RE: [Coq-Club] Weird installation error in OS X Mavericks, Soegtrop, Michael, 02/25/2015
Archive powered by MHonArc 2.6.18.