coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Using ltac:(admit) to define terms.

From: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Using ltac:(admit) to define terms.
Date: Mon, 11 Jul 2016 17:53:35 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=arthur.aa AT gmail.com; spf=Pass smtp.mailfrom=arthur.aa AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f45.google.com
Ironport-phdr: 9a23:1yIMER+rPLXwIv9uRHKM819IXTAuvvDOBiVQ1KB91O4cTK2v8tzYMVDF4r011RmSDN2dsK8P1LGempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47AblHf6ke/8SQVUk2mc1EkfqKuR8WN1Iye7KObw9XreQJGhT6wM/tZDS6dikHvjPQQmpZoMa0ryxHE8TNicuVSwn50dxrIx06vru/5xpNo8jxRtvQ97IYAFPyiJ+VrBYBfWR8hKige4NDh/U3IShLK7X8BWE0XlABJCk7L9kepcI32t37TrPZ9xTPSFN/7U704Xnyu4u9CTRjyiSJPYzcj7GHKkIp5hYpUpRugo1p0xIuCM9LdD+Z3Yq6IJYBSfmFGRMsEEnUZWo4=

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?

[Coq-Club] Using ltac:(admit) to define terms., Arthur Azevedo de Amorim, 07/11/2016
- Re: [Coq-Club] Using ltac:(admit) to define terms., Jonathan Leivent, 07/11/2016
  - Re: [Coq-Club] Using ltac:(admit) to define terms., Jonathan Leivent, 07/11/2016