Stream: Coq users

Topic: ✔ Error using theorem application as a Goal

Jiahong Lee (Jun 27 2022 at 06:40):

Thanks! I'll reach there soon. Currently at last chapter of SF volume 0.

I'll consider my original question as solved.

Notification Bot (Jun 27 2022 at 06:40):

Jiahong Lee has marked this topic as resolved.

Pierre Courtieu (Jun 27 2022 at 07:36):

I think it is worth saying that « being true » or « being True » is very misleading here. Proving a theorem does not mean it is (equal to) True or true. Like not at all.

Last updated: Feb 06 2023 at 12:04 UTC