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

chore: remove workaround

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-22 07:06:09 -07:00
parent a919349c80
commit 2a393cd4ab
1 changed files with 0 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Attributes.lean
View file

@ -43,8 +43,6 @@ structure AttributeImplCore :=
structure AttributeImpl extends AttributeImplCore :=
(add (decl : Name) (args : Syntax) (persistent : Bool) : AttrM Unit)
-- TODO: shouldn't be necessary
(applicationTime := AttributeApplicationTime.afterTypeChecking)
instance : Inhabited AttributeImpl :=
⟨{ name := arbitrary _, descr := arbitrary _, add := fun env _ _ _ => pure () }⟩
@ -323,8 +321,6 @@ structure ParametricAttributeImpl (α : Type) extends AttributeImplCore :=
(getParam : Name → Syntax → AttrM α)
(afterSet : Name → α → AttrM Unit := fun env _ _ => pure ())
(afterImport : Array (Array (Name × α)) → ImportM Unit := fun _ => pure ())
-- TODO: shouldn't be necessary
(applicationTime := AttributeApplicationTime.afterTypeChecking)
def registerParametricAttribute {α : Type} [Inhabited α] (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
let ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {