From 9064e6a7715671dec1b987d632e14cd63493be91 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sat, 28 Oct 2023 16:33:27 -0400 Subject: [PATCH] Minor macro_rules bug fix --- Duper/Tactic.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean index b9cc02e..7eb73ff 100644 --- a/Duper/Tactic.lean +++ b/Duper/Tactic.lean @@ -484,12 +484,12 @@ macro_rules -- XXX comments indicate which portions of the duper invocation are `(tactic| duper [] (portfolioMode := false) (portfolioInstance := 0)) -- 0 is default portfolio instance | `(tactic| duper (portfolioMode := $pMode) (portfolioInstance := $val)) => -- 011 (Casing on $pMode handled in evalDuper) `(tactic| duper [] (portfolioMode := $pMode) (portfolioInstance := $val)) -| `(tactic| duper [$facts]) => -- 100 (portfolioMode is enabled by default if portfolioInstance is not specified) - `(tactic| duper [$facts] (portfolioMode := true)) -| `(tactic| duper [$facts] (portfolioInstance := $val)) => -- 101 (portfolioMode is false if portfolioInstance is specified) - `(tactic| duper [$facts] (portfolioMode := false) (portfolioInstance := $val)) -| `(tactic| duper [$facts] (portfolioMode := false)) => -- 110 (portfolioMode := false) (110 (portfolioMode := true) case handled in evalDuper) - `(tactic| duper [$facts] (portfolioMode := false) (portfolioInstance := 0)) -- 0 is default portfolio instance +| `(tactic| duper [$facts,*]) => -- 100 (portfolioMode is enabled by default if portfolioInstance is not specified) + `(tactic| duper [$facts,*] (portfolioMode := true)) +| `(tactic| duper [$facts,*] (portfolioInstance := $val)) => -- 101 (portfolioMode is false if portfolioInstance is specified) + `(tactic| duper [$facts,*] (portfolioMode := false) (portfolioInstance := $val)) +| `(tactic| duper [$facts,*] (portfolioMode := false)) => -- 110 (portfolioMode := false) (110 (portfolioMode := true) case handled in evalDuper) + `(tactic| duper [$facts,*] (portfolioMode := false) (portfolioInstance := 0)) -- 0 is default portfolio instance /-- Entry point for calling duper. Facts should consist of lemmas supplied by the user, instanceMaxHeartbeats should indicate how many heartbeats duper should run for before timing out (if instanceMaxHeartbeats is set to 0, then duper will run until it is timed out