add file

SimonGuilloud · SimonGuilloud · commit c3bff668c3f0 · 2026-02-09T11:11:07.000+01:00
diff --git a/lisa-sets/src/main/scala/lisa/hol/HOLSteps.scala b/lisa-sets/src/main/scala/lisa/hol/HOLSteps.scala
@@ -523,7 +523,7 @@ object HOLSteps extends lisa._HOL {
         case _ =>
           return proof.InvalidProofTactic(s"The Expr[Ind] should be of the form (λx. t) x")
     }
-  }
+  } 
 
 
   // λ(x, t*x) === t

Original file line number	Diff line number	Diff line change
`@@ -523,7 +523,7 @@ object HOLSteps extends lisa._HOL {`
`523`	`523`	`case _ =>`
`524`	`524`	`return proof.InvalidProofTactic(s"The Expr[Ind] should be of the form (λx. t) x")`
`525`	`525`	`}`
`526`		`- }`
	`526`	`+ }`
`527`	`527`
`528`	`528`
`529`	`529`	`// λ(x, t*x) === t`