Stream: Coq users

Topic: ✔ SProp: error at Qed

view this post on Zulip Olivier Laurent (Dec 30 2021 at 15:33):

I am not familiar at all with SProp. Is it normal to get an error message at Qed:

Lemma test_sprop : (forall P : Prop, P) -> forall S : SProp, S.
intros HP S.
apply HP.
Fail Qed.

view this post on Zulip Gaëtan Gilbert (Dec 30 2021 at 15:34):


view this post on Zulip Notification Bot (Dec 30 2021 at 17:13):

Olivier Laurent has marked this topic as resolved.

Last updated: Jun 25 2024 at 14:01 UTC