Gergely Buday (Jul 14 2020 at 06:27): Gergely Buday (Jul 14 2020 at 06:27):I have the following in a file:
Definition Admit {A} : A. admit. Defined.
Coq does not accept it. What is the meaning of this definition?
How can I fix this?
jco (Jul 14 2020 at 06:31):try Definition Admit {A}: A. Admitted. admit is for "shelving" a goal, but it won't let you define the proof if you use it...it's useful if you want to move on to other goals to see if some idea is worth pursuing etc
Gergely Buday (Jul 14 2020 at 06:33):I see, thanks. What is {A} : A ?
jco (Jul 14 2020 at 06:41):I'm probably not the best one to explain these details as I'm still learning them myself, but I believe {A} is say that it is is a parameter that can be left implicit for type resolution, :A is saying that it is all of type A
jco (Jul 14 2020 at 06:42):Print Admit. gives: *** [ Admit : forall A : Type, A ]
Paolo Giarrusso (Jul 14 2020 at 08:00):This Admit is a relative of the normal admit — if also lets you prove anything
Paolo Giarrusso (Jul 14 2020 at 08:02):All that @jco said is correct
Paolo Giarrusso (Jul 14 2020 at 08:07):To expand on that, if you use “apply Admit” instead of “admit” to skip a goal, then you can still close the proof with Qed/Defined, even if the proof is not actually done.
Last updated: Oct 13 2024 at 01:02 UTC