The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 07/11/2016 02:07 PM, Jonathan Leivent wrote:
> 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.

BTW: if you do the following, you bypass the can't infer error and get 
the Defined/Admitted one:

Definition exercise : nat := ltac:(abstract admit).

Error: Attempt to save a proof with given up goals. If this is really 
what you want to do, use Admitted in place of
Qed. (in proof anonymous_subproof)

This is because admit is now a synonym for the give_up tactic.

FYI: many bikes were shed on coqdev over whether to do it this way or 
not ;-)

-- Jonathan

> 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?