Skip to content
Snippets Groups Projects
Commit 797223f3 authored by SimonGuilloud's avatar SimonGuilloud
Browse files

Trying to satisfy the CI, 6.

parent 6a25924b
No related branches found
No related tags found
6 merge requests!62Easy tactics,!58Easy tactics,!55Front integration and various changes,!54Front integration,!53Front integration,!52Front integration
......@@ -211,7 +211,7 @@ abstract class Library(val theory: RunningTheory) {
def DEFINE(symbol: String, vars: VariableLabel*): FunSymbolDefine = FunSymbolDefine(symbol, vars)
/**
* For a definition of the type f(x) := term, construct the required proof !y. y = term.
* For a definition of the type f(x) := term, construct the required proof ?!y. y = term.
*/
private def simpleFunctionDefinition(expression: LambdaTermTerm, out: VariableLabel): Proof = {
val x = out
......
......@@ -12,7 +12,7 @@ import lisa.kernel.proof.SequentCalculus.*
import lisa.settheory.AxiomaticSetTheory.*
import lisa.kernel.proof.SCProofCheckerJudgement.*
import org.scalatest.funsuite.AnyFunSuite
import me.cassayre.florian.masterproject.util.SCProofBuilder.{*, given}
import me.cassayre.florian.masterproject.util.SCProofBuilder.{_, given}
import util.chaining.*
import scala.util.{Failure, Success, Try}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment