vscode-lean4 icon indicating copy to clipboard operation
vscode-lean4 copied to clipboard
verified publisher icon leanprover

RFC: inherit_doc hover support

Open alok opened this issue 1 year ago • 0 comments

Proposal

Add hover support to defs with inherit_doc that forwards the inherited doc + type sig of current def.

alok avatar May 09 '24 08:05 alok