Implement collectEpsilons

epfl-lara · Nov 6, 2024 · 2a71ded · 2a71ded
1 parent 9b8e78f
commit 2a71ded
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/lisa-utils/src/main/scala/lisa/utils/prooflib/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/utils/prooflib/BasicStepTactic.scala
@@ -1003,7 +1003,8 @@ object BasicStepTactic {
    * fail. Use [[RightEpsilon.withParameters]] instead.
    */
   object RightEpsilon extends ProofTactic with ProofFactSequentTactic {
-    def collectEpsilons(in: F.Expr[?]): Set[F.Expr[F.Term]] = ???
+    def collectEpsilons(in: F.Expr[?]): Set[F.Expr[F.Term]] = 
+      in.collect { case e @ F.ε(_, _) => e.asInstanceOf[F.Expr[F.Term]] }.toSet
 
     def withParameters(using lib: Library, proof: lib.Proof)(phi: F.Expr[F.Formula], x: F.Variable[F.Term], t: F.Expr[F.Term])(premise: proof.Fact)(bot: F.Sequent): proof.ProofTacticJudgement = {
       lazy val premiseSequent = proof.getSequent(premise).underlying