feat: suggestions don't included deprecated theorems (#11125)
This PR adds a filter for premise selectors to ensure deprecated theorems are not returned.
This commit is contained in:
parent
c7652413db
commit
d47b474e41
1 changed files with 2 additions and 0 deletions
|
|
@ -9,6 +9,7 @@ prelude
|
|||
public import Lean.Elab.Command
|
||||
public import Lean.Meta.Eval
|
||||
public import Lean.Meta.CompletionName
|
||||
public import Lean.Linter.Deprecated
|
||||
public import Init.Data.Random
|
||||
|
||||
/-!
|
||||
|
|
@ -299,6 +300,7 @@ def isDeniedPremise (env : Environment) (name : Name) : Bool := Id.run do
|
|||
if name == ``sorryAx then return true
|
||||
if name.isInternalDetail then return true
|
||||
if Lean.Meta.isInstanceCore env name then return true
|
||||
if Lean.Linter.isDeprecated env name then return false
|
||||
if (nameDenyListExt.getState env).any (fun p => name.anyS (· == p)) then return true
|
||||
if let some moduleIdx := env.getModuleIdxFor? name then
|
||||
let moduleName := env.header.moduleNames[moduleIdx.toNat]!
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue