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.
Proof.
intros HP S.
apply HP.
Fail Qed.

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

yes

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

Olivier Laurent has marked this topic as resolved.

Last updated: Apr 19 2024 at 05:01 UTC