Stream: Coq users

Topic: Admitted not found in environment


view this post on Zulip Sam Stites (Jul 01 2021 at 19:50):

Hi all, I don't have the Admitted keyword in scope for a project I am working on. Could anyone tell me where it is located?

view this post on Zulip Gaëtan Gilbert (Jul 01 2021 at 20:26):

it's a command not a keyword
what are you doing?

view this post on Zulip Sam Stites (Jul 01 2021 at 21:13):

I'm just running trying to write a function in the CompCert code base

view this post on Zulip Paolo Giarrusso (Jul 02 2021 at 00:38):

You're likely using it with the wrong syntax; you can't write 1 + Admitted, the syntax is like that of Qed or Defined.

view this post on Zulip Sam Stites (Jul 02 2021 at 01:43):

I'm using it as a standalone statement! Admitted can be in a term, right? I was trying to write:

Definition globdef_to_type (gty: AST.globdef CStan.fundef type) : type :=
  Admitted.

With an error of: Error: The reference Admitted was not found in the current environment.

I am just working around this for the time being. I know that CompCert has some particular infrastructure, but I was sort of assuming Admitted would be in scope.

view this post on Zulip Joshua Grosso (Jul 02 2021 at 01:49):

Sam Stites said:

I'm using it as a standalone statement! Admitted can be in a term, right? I was trying to write:

Definition globdef_to_type (gty: AST.globdef CStan.fundef type) : type :=
  Admitted.

With an error of: Error: The reference Admitted was not found in the current environment.

I am just working around this for the time being. I know that CompCert has some particular infrastructure, but I was sort of assuming Admitted would be in scope.

I think that Admitted. only works in the context of a proof, so if you replace := with . it should work.

view this post on Zulip Joshua Grosso (Jul 02 2021 at 01:50):

(Hmm, I wonder if ltac:(admit) or ltac:(give_up) are valid terms? EDIT: Nope :frown: )

view this post on Zulip Jason Gross (Jul 02 2021 at 02:00):

Joshua Grosso said:

(Hmm, I wonder if ltac:(admit) or ltac:(give_up) are valid terms? EDIT: Nope :frown: )

I think that if you use Program Definition instead (or if you do Require Import Coq.Compat.AdmitAxiom), then this should work

view this post on Zulip Sam Stites (Jul 02 2021 at 02:02):

Joshua Grosso said:
I think that Admitted. only works in the context of a proof, so if you replace := with . it should work.

that's it -- thank you!


Last updated: Mar 28 2024 at 22:01 UTC