Stream: Coq users

Topic: Interesting definition


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Gergely Buday (Jul 14 2020 at 06:33):

I see, thanks. What is {A} : A ?

view this post on Zulip 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

view this post on Zulip jco (Jul 14 2020 at 06:42):

Print Admit. gives: *** [ Admit : forall A : Type, A ]

view this post on Zulip Paolo Giarrusso (Jul 14 2020 at 08:00):

This Admit is a relative of the normal admit — if also lets you prove anything

view this post on Zulip Paolo Giarrusso (Jul 14 2020 at 08:02):

All that @jco said is correct

view this post on Zulip 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: Jan 29 2023 at 04:05 UTC