The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I think the point of the new way admit works is that there is no way to 
make

> Definition exercise : nat := ltac:(admit).
work via direct usage of admit - because the result would be Defined 
instead of just Admitted.  However, the error about not being able to 
infer an existential variable of type "nat" happens earlier than that - 
which means that any way of fixing that error will just run afoul of the 
Defined/Admitted issue.

To get around this, you will have to define something that is Admitted 
or itself an axiom, then use that - which is IMHO what the new rules 
about admit are trying to force you to do - declare your intentions to 
leave something undefined instead of relying on the standard library to 
hide those intentions for you.

-- Jonathan


On 07/11/2016 01:53 PM, Arthur Azevedo de Amorim wrote:
> Dear list,
>
> In the Software Foundations textbook, we define an "admit" axiom that we
> use to leave out parts of definitions in exercises:
>
> Axiom admit : forall {T : Type}, T.
> (* Replace "admit" with answer here *)
> Definition exercise : nat := admit.
>
> We were wondering whether we could remove this definition in favor of just
> using ltac:(admit). Unfortunately, this causes Coq to complain about
> existential variables:
>
> Definition exercise : nat := ltac:(admit).
> > Toplevel input, characters 0-39:
> > Error: Cannot infer an existential variable of type "nat".
> Is there anyway of making this work?