From 40d00f252b0b6557f8d869a29715c1fd44b017f3 Mon Sep 17 00:00:00 2001
From: SimonGuilloud <sim-guilloud@bluewin.ch>
Date: Sun, 15 May 2022 23:22:18 +0200
Subject: [PATCH] Correction of small error regarding function and predicate
definition.
---
src/main/scala/lisa/kernel/proof/RunningTheory.scala | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index a67c5615..0f9c4ce9 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -107,7 +107,7 @@ class RunningTheory {
def makePredicateDefinition(label: ConstantPredicateLabel, args: Seq[VariableLabel], phi: Formula): RunningTheoryJudgement[this.PredicateDefinition] = {
if (belongsToTheory(phi))
if (!isAcceptedPredicateLabel(label))
- if (phi.freeVariables.isEmpty && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
+ if (phi.freeVariables.subsetOf(args.toSet) && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
val newDef = PredicateDefinition(label, args, phi)
predDefinitions.update(label, Some(newDef))
RunningTheoryJudgement.ValidJustification(newDef)
@@ -133,7 +133,7 @@ class RunningTheory {
def makeFunctionDefinition(proof: SCProof, justifications:Seq[Justification], label: ConstantFunctionLabel, args: Seq[VariableLabel], out: VariableLabel, phi: Formula): RunningTheoryJudgement[this.FunctionDefinition] = {
if (belongsToTheory(phi))
if (!isAcceptedFunctionLabel(label))
- if (phi.freeVariables.isEmpty && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
+ if (phi.freeVariables.subsetOf(args.toSet + out) && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
if (proof.imports.forall(i => justifications.exists( j => isSameSequent(i, sequentFromJustification(j)))))
val r = SCProofChecker.checkSCProof(proof)
r match {
--
GitLab