diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Progress/Base.lean | 4 | ||||
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 4 |
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 |