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?
it's a command not a keyword
what are you doing?
I'm just running trying to write a function in the CompCert code base
You're likely using it with the wrong syntax; you can't write 1 + Admitted, the syntax is like that of Qed or Defined.
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.
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.
(Hmm, I wonder if ltac:(admit)
or ltac:(give_up)
are valid terms? EDIT: Nope :frown: )
Joshua Grosso said:
(Hmm, I wonder if
ltac:(admit)
orltac:(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
Joshua Grosso said:
I think thatAdmitted.
only works in the context of a proof, so if you replace:=
with.
it should work.
that's it -- thank you!
Last updated: Oct 13 2024 at 01:02 UTC