Lukas Stevens (Sep 29 2021 at 16:06): Lukas Stevens (Sep 29 2021 at 16:06):When I call Thm.hyps_of I get a list of open hypotheses of a theorem. Additionally, I may have a context that has the premises given by Assumption.all_prems_of. Is there an efficient way to determine whether all hypotheses of the theorem are also premises of the context and can therefore considered to be closed (w.r.t the context)?
Lukas Stevens (Sep 30 2021 at 16:10):I think what I really need is to discharge those assumptions. Normally, the function Assumption.export seems to be the right tool for the job. However, I only have one context so what is the target context? Just the global context?
Last updated: Dec 21 2024 at 16:20 UTC