Zulip Chat Archive

Stream: general

Topic: ctags

Julian Berman (Oct 27 2020 at 23:24):

I don't suppose anyone has scrapped together a ctags language definition for lean? Messy/not fully accurate is obviously fine, just wondering if anyone has done so already.

Simon Hudon (Oct 27 2020 at 23:25):

Not that I know of. @Gabriel Ebner ?

Yury G. Kudryashov (Oct 27 2020 at 23:33):

I wonder if we can write a ctags file during compilation, then distribute it with oleans.

Yury G. Kudryashov (Oct 27 2020 at 23:38):

Or something like Coq glob file https://coq.inria.fr/refman/using/tools/coqdoc.html#hyperlinks

Last updated: Dec 20 2023 at 11:08 UTC