From f49250c90651c60f0fdf1955aad2fffe44541388 Mon Sep 17 00:00:00 2001 From: Robby Date: Thu, 22 Feb 2024 08:34:32 -0600 Subject: [PATCH] Use an alternative form of Let {(...) => SubProof(...)}: SubProof{(...) => (...)}. --- upgrader/src/main/scala/Upgrader.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/upgrader/src/main/scala/Upgrader.scala b/upgrader/src/main/scala/Upgrader.scala index c1a2d52..097fe1a 100644 --- a/upgrader/src/main/scala/Upgrader.scala +++ b/upgrader/src/main/scala/Upgrader.scala @@ -455,7 +455,7 @@ final class Upgrader(isAuto: B, input: Predef.String, implyOp: String, var invCo val steps = step.proofStep val ss = for (i <- 0 until steps.size) yield translateProofStep(steps.get(i)) if (step.ID != null && step.ate != null) { - st"""${step.sub.getText} Let { (${step.ID.getText}: ${if (step.`type` == null) st"T" else translateType(step.`type`)}) => SubProof( + st"""${step.sub.getText} SubProof { (${step.ID.getText}: ${if (step.`type` == null) st"T" else translateType(step.`type`)}) => ( | ${step.assume.getText} Assume(${translateFormula(step.formula, None())})${if (ss.nonEmpty) "," else ""} | ${(ss, ",\n")} |)}""" @@ -465,7 +465,7 @@ final class Upgrader(isAuto: B, input: Predef.String, implyOp: String, var invCo | ${(ss, ",\n")} |)""" } else { - st"""${step.sub.getText} Let { (${step.ID.getText}: ${if (step.`type` == null) st"T" else translateType(step.`type`)}) => SubProof( + st"""${step.sub.getText} SubProof { (${step.ID.getText}: ${if (step.`type` == null) st"T" else translateType(step.`type`)}) => ( | ${(ss, ",\n")} |)}""" }