Avoid checking whether proofs are required or not if we don't care ab…

…out the result. fixes #86
SReichelt · Jan 3, 2021 · ea7bf9f · ea7bf9f
1 parent 0c95183
commit ea7bf9f
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/src/shared/logics/hlm/checker.ts b/src/shared/logics/hlm/checker.ts
@@ -1443,6 +1443,9 @@ export class HLMDefinitionChecker {
   }
 
   private checkMultiGoalProof(object: Object, proof: FmtHLM.ObjectContents_Proof | undefined, parameters: Fmt.ParameterList | undefined, goals: Fmt.Expression[], context: HLMCheckerContext): void {
+    if (!proof && !this.options.warnAboutMissingProofs) {
+      return;
+    }
     if (parameters) {
       if (proof) {
         if (!proof.parameters) {
@@ -1468,8 +1471,7 @@ export class HLMDefinitionChecker {
           object = proof;
         }
         this.checkProofValidity(object, proof, newGoals, context);
-      } else if (this.options.warnAboutMissingProofs
-                 && !newGoals.some((goal: Fmt.Expression) => this.utils.isTrueFormula(goal))) {
+      } else if (!newGoals.some((goal: Fmt.Expression) => this.utils.isTrueFormula(goal))) {
         this.message(object, parameters || !newGoals.length ? 'Proof required' : `Proof of ${newGoals.join(' or ')} required`, Logic.DiagnosticSeverity.Warning);
       }
     });