summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Progress
diff options
context:
space:
mode:
authorSon Ho2023-07-25 16:26:08 +0200
committerSon Ho2023-07-25 16:26:08 +0200
commit1854c631a6a7a3f8d45ad18e05547f9d3782c3ee (patch)
tree270e16d5c106d00b0e18520bf89d05d1e202cdb6 /backends/lean/Base/Progress
parent876137dff361620d8ade1a4ee94fa9274df0bdc6 (diff)
Make progress on the hashmap properties
Diffstat (limited to 'backends/lean/Base/Progress')
-rw-r--r--backends/lean/Base/Progress/Base.lean4
-rw-r--r--backends/lean/Base/Progress/Progress.lean4
2 files changed, 4 insertions, 4 deletions
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index b54bdf7a..6f820a84 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -81,8 +81,8 @@ section Methods
let (fExpr, f, args) ← do
if mf.isConst ∧ mf.constName = ``Bind.bind then do
-- Dive into the bind
- let fExpr := margs.get! 4
- fExpr.consumeMData.withApp fun f args => pure (fExpr, f, args)
+ let fExpr := (margs.get! 4).consumeMData
+ fExpr.withApp fun f args => pure (fExpr, f, args)
else pure (mExpr, mf, margs)
trace[Progress] "After stripping the arguments of the function call:\n- f: {f}\n- args: {args}"
if ¬ f.isConst then throwError "Not a constant: {f}"
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index a281f1d2..a2c7764f 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -58,9 +58,9 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
let (thBody, _) ← destEq thBody
trace[Progress] "After splitting equality: {thBody}"
-- There shouldn't be any existential variables in thBody
- pure thBody
+ pure thBody.consumeMData
-- Match the body with the target
- trace[Progress] "Matching `{thBody}` with `{fExpr}`"
+ trace[Progress] "Matching:\n- body:\n{thBody}\n- target:\n{fExpr}"
let ok ← isDefEq thBody fExpr
if ¬ ok then throwError "Could not unify the theorem with the target:\n- theorem: {thBody}\n- target: {fExpr}"
let mgoal ← Tactic.getMainGoal