fix: apply after-compilation attributes to inductive/structure decls
Attributes with `AttributeApplicationTime.afterCompilation` were silently not applied to `inductive` and `structure` declarations.
This commit is contained in:
Jannis Limperg
Leonardo de Moura
parent
4a1885f997
commit
6dc5ddac35
3 changed files with 80 additions and 75 deletions
|
|
@ -778,7 +778,7 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
|
|||
for ctor in view.ctors do
|
||||
Term.addTermInfo' ctor.ref[2] (← mkConstWithLevelParams ctor.declName) (isBinder := true)
|
||||
-- We need to invoke `applyAttributes` because `class` is implemented as an attribute.
|
||||
Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking
|
||||
Term.applyAttributesAt view.declName view.modifiers.attrs .afterTypeChecking
|
||||
|
||||
private def applyDerivingHandlers (views : Array InductiveView) : CommandElabM Unit := do
|
||||
let mut processed : NameSet := {}
|
||||
|
|
@ -803,5 +803,8 @@ def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
|
|||
for view in views do
|
||||
mkInjectiveTheorems view.declName
|
||||
applyDerivingHandlers views
|
||||
runTermElabM view0.declName fun vars => withRef ref do
|
||||
for view in views do
|
||||
Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation
|
||||
|
||||
end Lean.Elab.Command
|
||||
|
|
|
|||
|
|
@ -904,6 +904,8 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
|
|||
mkInjectiveTheorems declName
|
||||
return declName
|
||||
derivingClassViews.forM fun view => view.applyHandlers #[declName]
|
||||
runTermElabM declName fun _ =>
|
||||
Term.applyAttributesAt declName modifiers.attrs .afterCompilation
|
||||
|
||||
builtin_initialize registerTraceClass `Elab.structure
|
||||
|
||||
|
|
|
|||
|
|
@ -1,77 +1,3 @@
|
|||
jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.arrow G T EG getCtx
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
|
||||
(@EGrfl
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
|
||||
(@EGrfl
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
Γ✝ : G
|
||||
⊢ G
|
||||
jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
Γ✝ : G
|
||||
⊢ G
|
||||
jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
Γ✝ : G
|
||||
⊢ G
|
||||
jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
Γ✝ : G
|
||||
⊢ G
|
||||
jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
|
||||
context:
|
||||
|
|
@ -122,3 +48,77 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
|||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
Γ✝ : G
|
||||
⊢ G
|
||||
jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
Γ✝ : G
|
||||
⊢ G
|
||||
jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.arrow G T EG getCtx
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
|
||||
(@EGrfl
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
|
||||
(@EGrfl
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
Γ✝ : G
|
||||
⊢ G
|
||||
jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
Γ✝ : G
|
||||
⊢ G
|
||||
jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
Γ✝ : G
|
||||
⊢ G
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue