Stream: Isabelle/ML

Topic: term export argument in `Assumption.export`


view this post on Zulip Mathias Fleury (Nov 26 2021 at 06:43):

I have only used Assumption.import and co (the difference is that they work on a proper proof context), but my guess is that this comes from variables you declare locally (the one that become ?x in the goal) that can conflict with global constants.

view this post on Zulip Manuel Eberl (Nov 26 2021 at 09:29):

It's a good idea to ask such questions on the mailing list, since the best person to answer them is probably Makarius, and he boycotts Zulip.

view this post on Zulip Qiyuan Xu (Nov 26 2021 at 14:17):

Mathias Fleury said:

I have only used Assumption.import and co (the difference is that they work on a proper proof context), but my guess is that this comes from variables you declare locally (the one that become ?x in the goal) that can conflict with global constants.

sorry, do you mean the import function in Assumption structure? I don't find that function in file src/Pure/assumption.ML

view this post on Zulip Mathias Fleury (Nov 26 2021 at 14:18):

Sorry I meant Assumption.add_assumes


Last updated: Jul 15 2022 at 23:21 UTC