Notification Bot (May 31 2022 at 05:26): Notification Bot (May 31 2022 at 05:26):Kiran Gopinathan has marked this topic as resolved.
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