diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 0e5820fcd848..1c34873dbdd7 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -11,10 +11,10 @@ namespace Lean.Elab open Meta /-- Assign `mvarId := sorry` -/ -def admitGoal (mvarId : MVarId) : MetaM Unit := +def admitGoal (mvarId : MVarId) (synthetic : Bool := true): MetaM Unit := mvarId.withContext do let mvarType ← inferType (mkMVar mvarId) - mvarId.assign (← mkLabeledSorry mvarType (synthetic := true) (unique := true)) + mvarId.assign (← mkLabeledSorry mvarType (synthetic := synthetic) (unique := true)) def goalsToMessageData (goals : List MVarId) : MessageData := MessageData.joinSep (goals.map MessageData.ofGoal) m!"\n\n" diff --git a/src/Lean/Elab/Tactic/LibrarySearch.lean b/src/Lean/Elab/Tactic/LibrarySearch.lean index 1a7e6bcd0390..b1d51c06a88c 100644 --- a/src/Lean/Elab/Tactic/LibrarySearch.lean +++ b/src/Lean/Elab/Tactic/LibrarySearch.lean @@ -48,7 +48,7 @@ def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireCl addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta (checkState? := initialState) (addSubgoalsMsg := true) (tacticErrorAsInfo := true) if suggestions.isEmpty then logError "apply? didn't find any relevant lemmas" - admitGoal goal + admitGoal goal (synthetic := false) @[builtin_tactic Lean.Parser.Tactic.exact?] def evalExact : Tactic := fun stx => do diff --git a/tests/lean/librarySearch.lean b/tests/lean/librarySearch.lean index 44a7de15e803..b0a20fafa432 100644 --- a/tests/lean/librarySearch.lean +++ b/tests/lean/librarySearch.lean @@ -275,3 +275,7 @@ error: apply? didn't find any relevant lemmas -/ #guard_msgs in example {α : Sort u} (x y : α) : Eq x y := by apply? + +-- Verify that there is a `sorry` warning when `apply?` closes the goal. +#guard_msgs (drop info) in +example : False := by apply? diff --git a/tests/lean/librarySearch.lean.expected.out b/tests/lean/librarySearch.lean.expected.out index e69de29bb2d1..1dc39a98a4df 100644 --- a/tests/lean/librarySearch.lean.expected.out +++ b/tests/lean/librarySearch.lean.expected.out @@ -0,0 +1 @@ +librarySearch.lean:281:0-281:7: warning: declaration uses 'sorry'