How do I stop Holmake from proving false theorems?!
The default behaviour of Holmake is to cause failing proofs (from calls to prove and store_thm) to be asserted as true with mk_thm (such results get oracle tags recording this fact). This behaviour allows for more of a script file to be checked because the first failing proof doesn’t abort the script. If you don’want this behaviour, use the –qof (“quit on failure”) flag to Holmake, or use an OPTIONS = QUIT_ON_FAILURE line in a Holmakefile.
Related Questions
- Ive been using the IsNull function but it seems to be ignoring the second parameter (just returning True or False instead). Is this function supported and/or is there an alternative?
- What are the standards for proving fraud under the False Claims Act?
- Can a person with epilepsy have a false negative EEG?
