Kiran Gopinathan has marked this topic as resolved.
@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