You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In the situation where a user wants to recheck a .thm file, the user would not know that some theorems were not really proved (if skip were used) if he doesn't read it explicitly in the file (in the .thm or in the output file). Wouldn't that be a problem in case of rechecking a large set of files where the user will not, in practice, read through every proof script?
The text was updated successfully, but these errors were encountered:
innofarah
changed the title
Notify/warn the user when a "skip" is used in a .thm file?
Notify/warn the user when a skip is used in a .thm file?
Apr 26, 2022
I think it is good to provide a printed warning that a skip appears in the proof of a theorem when checking a theorem file. I believe this would only need to appear when someone runs the Abella command at the command line with a .thm file as its argument.
In the situation where a user wants to recheck a .thm file, the user would not know that some theorems were not really proved (if skip were used) if he doesn't read it explicitly in the file (in the .thm or in the output file). Wouldn't that be a problem in case of rechecking a large set of files where the user will not, in practice, read through every proof script?
The text was updated successfully, but these errors were encountered: