Stream: Coq devs & plugin devs

Topic: SProp breaks subject reduction?


view this post on Zulip Jason Gross (Mar 26 2021 at 20:43):

Is it known that subject reduction in Coq is broken in the presence of SProp?

view this post on Zulip Enrico Tassi (Mar 26 2021 at 20:44):

This one is for @Gaëtan Gilbert

view this post on Zulip Jason Gross (Mar 26 2021 at 20:46):

Reported as https://github.com/coq/coq/issues/14015


Last updated: Jun 23 2024 at 01:02 UTC