Stream: Coq users

Topic: ✔ Computing through opaque definitions

view this post on Zulip Notification Bot (May 31 2022 at 05:26):

Kiran Gopinathan has marked this topic as resolved.

view this post on Zulip Michael Soegtrop (May 31 2022 at 07:05):

@Gaëtan Gilbert : thanks for the nice example! To summarize: if I replace the Qed for T.v with Defined, M fails to type check as argument for F. But if I close T.v with Qed, F M does type check and this means it must not be allowed to undo the opaqueness of T.v. Not easy to get these things right, as it looks ...

Last updated: Jan 27 2023 at 02:04 UTC