/-
Copyright (c) 2022 Gabriel Ebner. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner
-/
import Lean.Attributes

/-- Get the list of declarations tagged with the tag attribute `attr`. -/
def 
Lean.TagAttribute.getDecls: TagAttribute → Environment → Array Name
Lean.TagAttribute.getDecls (
attr: TagAttribute
attr : 
TagAttribute: Type
TagAttribute) (
env: Environment
env : 
Environment: Type
Environment) : 
Array: Type ?u.6 → Type ?u.6
Array 
Name: Type
Name :=
  
core: PersistentEnvExtensionState Name NameSet → Array Name
core <| 
attr: TagAttribute
attr.
ext: TagAttribute → PersistentEnvExtension Name Name NameSet
ext.
toEnvExtension: {α β σ : Type} → PersistentEnvExtension α β σ → EnvExtension (PersistentEnvExtensionState α σ)
toEnvExtension.
getState: {σ : Type} → [inst : Inhabited σ] → EnvExtension σ → Environment → σ
getState 
env: Environment
env
where
  /-- Implementation of `TagAttribute.getDecls`. -/
  
core: PersistentEnvExtensionState Name NameSet → Array Name
core (
st: PersistentEnvExtensionState Name NameSet
st : 
PersistentEnvExtensionState: Type → Type → Type
PersistentEnvExtensionState 
Name: Type
Name 
NameSet: Type
NameSet) : 
Array: Type ?u.13 → Type ?u.13
Array 
Name: Type
Name := 
Id.run: {α : Type ?u.17} → Id α → α
Id.run do
    let mut 
decls: ?m.38
decls := 
st: PersistentEnvExtensionState Name NameSet
st.
state: {α σ : Type} → PersistentEnvExtensionState α σ → σ
state.
toArray: {α : Type ?u.43} → {cmp : α → α → Ordering} → RBTree α cmp → Array α
toArray
    for 
ds: ?m.143
ds in 
st: PersistentEnvExtensionState Name NameSet
st.
importedEntries: {α σ : Type} → PersistentEnvExtensionState α σ → Array (Array α)
importedEntries do
      
decls: ?m.152
decls := 
decls: ?m.149
decls ++ 
ds: ?m.143
ds
    
decls: ?m.326
decls