You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
AFAICT this is blocking the ability to have go-to-definition (for things like @[implementedBy foo] or @[builtinTactic Parser.Tactic.focus]) or hovers (on either implementedBy or foo) on attributes.
I think this entails adding an infoState field and MonadInfoTree instance to AttrM (making it not just a copy of CoreM), and threading through the state in applyAttributesCore.
The text was updated successfully, but these errors were encountered:
AFAICT this is blocking the ability to have go-to-definition (for things like
@[implementedBy foo]
or@[builtinTactic Parser.Tactic.focus]
) or hovers (on eitherimplementedBy
orfoo
) on attributes.I think this entails adding an
infoState
field andMonadInfoTree
instance toAttrM
(making it not just a copy ofCoreM
), and threading through the state inapplyAttributesCore
.The text was updated successfully, but these errors were encountered: