diff options
author | Son Ho | 2023-07-20 16:13:35 +0200 |
---|---|---|
committer | Son Ho | 2023-07-20 16:13:35 +0200 |
commit | 9b1498aa7fe014ac430467919504d35b0a688934 (patch) | |
tree | 6d259609c00ab2df8f3d2d3d3c073e35b5d3d0d6 /backends/lean | |
parent | e58872aa4dc31f0819fe17b13e6b7e4b0d9635c8 (diff) |
Fix a naming issue with progress
Diffstat (limited to '')
-rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 8 |
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" |