summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Progress
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base/Progress')
-rw-r--r--backends/lean/Base/Progress/Base.lean3
-rw-r--r--backends/lean/Base/Progress/Progress.lean11
2 files changed, 5 insertions, 9 deletions
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 03c80a42..0e46737f 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -1,5 +1,4 @@
import Lean
-import Std.Lean.HashSet
import Base.Utils
import Base.Primitives.Base
import Base.Extensions
@@ -111,7 +110,7 @@ section Methods
-- Collect all the free variables in the arguments
let allArgsFVars ← args.foldlM (fun hs arg => getFVarIds arg hs) HashSet.empty
-- Check if they intersect the fvars we introduced for the existentially quantified variables
- let evarsSet : HashSet FVarId := HashSet.ofArray (evars.map (fun (x : Expr) => x.fvarId!))
+ let evarsSet : HashSet FVarId := HashSet.empty.insertMany (evars.map (fun (x : Expr) => x.fvarId!))
let filtArgsFVars := allArgsFVars.toArray.filter (fun var => evarsSet.contains var)
if filtArgsFVars.isEmpty then pure ()
else
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 03d464d7..da601b73 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -131,7 +131,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
Tactic.focus do
let _ ←
tryTac
- (simpAt true {} []
+ (simpAt true {} #[] []
[``Primitives.bind_tc_ok, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
[hEq.fvarId!] (.targets #[] true))
-- It may happen that at this point the goal is already solved (though this is rare)
@@ -140,7 +140,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
else
trace[Progress] "goal after applying the eq and simplifying the binds: {← getMainGoal}"
-- TODO: remove this (some types get unfolded too much: we "fold" them back)
- let _ ← tryTac (simpAt true {} [] scalar_eqs [] .wildcard_dep)
+ let _ ← tryTac (simpAt true {} #[] [] scalar_eqs [] .wildcard_dep)
trace[Progress] "goal after folding back scalar types: {← getMainGoal}"
-- Clear the equality, unless the user requests not to do so
let mgoal ← do
@@ -346,11 +346,8 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
-- Not a local declaration: should be a theorem
trace[Progress] "With arg: theorem"
addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
- let cs ← resolveGlobalConstWithInfos id
- match cs with
- | [] => throwError "Could not find theorem {id}"
- | id :: _ =>
- pure (some (.Theorem id))
+ let some (.const name _) ← Term.resolveId? id | throwError m!"Could not find theorem: {id}"
+ pure (some (.Theorem name))
else pure none
let ids :=
let args := asArgs.getArgs