summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
authorSon Ho2023-07-20 16:13:35 +0200
committerSon Ho2023-07-20 16:13:35 +0200
commit9b1498aa7fe014ac430467919504d35b0a688934 (patch)
tree6d259609c00ab2df8f3d2d3d3c073e35b5d3d0d6 /backends/lean/Base
parente58872aa4dc31f0819fe17b13e6b7e4b0d9635c8 (diff)
Fix a naming issue with progress
Diffstat (limited to 'backends/lean/Base')
-rw-r--r--backends/lean/Base/Progress/Progress.lean8
1 files changed, 4 insertions, 4 deletions
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index dabd25b8..1c509775 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -118,17 +118,17 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids
match hPost with
| none => do return (.Error m!"Too many ids provided ({ids}): there is no postcondition to split")
| some hPost => pure hPost
- let curPostId := (← hPost.fvarId!.getDecl).userName
- let rec splitPost (hPost : Expr) (ids : List Name) : TacticM ProgressError := do
+ let rec splitPost (prevId : Name) (hPost : Expr) (ids : List Name) : TacticM ProgressError := do
match ids with
| [] => pure .Ok -- Stop
| nid :: ids => do
trace[Progress] "Splitting post: {hPost}"
-- Split
if ← isConj (← inferType hPost) then
- splitConjTac hPost (some (nid, curPostId)) (λ _ nhPost => splitPost nhPost ids)
+ splitConjTac hPost (some (prevId, nid)) (λ _ nhPost => splitPost nid nhPost ids)
else return (.Error m!"Too many ids provided ({nid :: ids}) not enough conjuncts to split in the postcondition")
- splitPost hPost ids
+ let curPostId := (← hPost.fvarId!.getDecl).userName
+ splitPost curPostId hPost ids
else return .Ok
match res with
| .Error _ => return res -- Can we get there? We're using "return"