max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: KeyedDeclsAttribute: preserve scopedness

Browse source
This commit is contained in:
Sebastian Ullrich 2021-03-13 13:17:13 +01:00
parent 03aea90981
commit 8f824ce141
1 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/KeyedDeclsAttribute.lean
View file

@ -125,13 +125,12 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDe
applicationTime := AttributeApplicationTime.afterCompilation
}
registerBuiltinAttribute {
name := df.name,
descr := df.descr,
add := fun constName stx persistent => do
name := df.name
descr := df.descr
add := fun constName stx attrKind => do
let key ← df.evalKey false stx
let val ← evalConstCheck γ df.valueTypeName constName
let env ← getEnv
setEnv <| ext.addEntry env { key := key, decl := constName, value := val },
ext.add { key := key, decl := constName, value := val } attrKind
applicationTime := AttributeApplicationTime.afterCompilation
}
pure { defn := df, tableRef := tableRef, ext := ext }