fix(frontend): Incorrect capture of binder term
This commit is contained in:
parent
3744cfaa96
commit
48b924fae2
|
@ -106,7 +106,7 @@ structure InfoWithContext where
|
|||
|
||||
private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do
|
||||
let infos ← t.findAllInfoM none fun i ctx? => match i with
|
||||
| .ofTermInfo { expectedType?, expr, stx, lctx, .. } => do
|
||||
| .ofTermInfo { expectedType?, expr, stx, lctx, isBinder := false, .. } => do
|
||||
let .some ctx := ctx? | return (false, true)
|
||||
if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then
|
||||
if expectedType?.isNone then
|
||||
|
|
Loading…
Reference in New Issue