summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Progress/Progress.lean13
1 files changed, 13 insertions, 0 deletions
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index ea38c630..f2a56e50 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -243,6 +243,9 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
-- Retrieve the goal
let mgoal ← Tactic.getMainGoal
let goalTy ← mgoal.getType
+ -- There might be uninstantiated meta-variables in the goal that we need
+ -- to instantiate (otherwise we will get stuck).
+ let goalTy ← instantiateMVars goalTy
trace[Progress] "goal: {goalTy}"
-- Dive into the goal to lookup the theorem
-- Remark: if we don't isolate the call to `withPSpec` to immediately "close"
@@ -458,6 +461,16 @@ namespace Test
f x = ok () := by
progress
+ /- The use of `right` introduces a meta-variable in the goal, that we
+ need to instantiate (otherwise `progress` gets stuck) -/
+ example {ty} {x y : Scalar ty}
+ (hmin : Scalar.min ty ≤ x.val + y.val)
+ (hmax : x.val + y.val ≤ Scalar.max ty) :
+ False ∨ (∃ z, x + y = ok z ∧ z.val = x.val + y.val) := by
+ right
+ progress keep _ as ⟨ z, h1 .. ⟩
+ simp [*, h1]
+
end Test
end Progress