Henry Story

Yep notices the same problem in agda-mode 0.2.3

I don't think so, but there seems to be interest in adding it. See [this conversation in zulip](https://agda.zulipchat.com/#narrow/stream/238741-general/topic/Editors.20%28emacs.2C.20vscode.2C.20.2E.2E.2E%29/near/214894065).

Here are a few examples of code from the Graphs library of [Agda Categories](https://github.com/agda/agda-categories/blob/7672b7a3185ae77467cc30e05dbe50b36ff2af8a/src/Categories/Category/Construction/Graphs.agda). [Line 229](https://github.com/agda/agda-categories/blob/7672b7a3185ae77467cc30e05dbe50b36ff2af8a/src/Categories/Category/Construction/Graphs.agda#L251) we have: ```agda M₁≡ : ∀ {A B} {f : A G.⇒ B} →...

yes, but it does not always work. Say I want to find out the value of `f` on line 249 of [Graphs from Agda Categories](https://github.com/agda/agda-categories/blob/7672b7a3185ae77467cc30e05dbe50b36ff2af8a/src/Categories/Category/Construction/Graphs.agda#L246). `C-c C-d` tells me it...

Btw here is a screenshot showing how one can hover over a part of the code in VSCode with Agda-mode when pressing the `command` key to get a definition. That...

For reference for people looking at this issue coming from emacs, this the info I get when hovering over the lambda variable `i`. Clearly that is not that useful. What...

What is needed is a general logic of how one merges linked data information. I have been working on this as part of my PhD on [co-operating.systems](https://co-operating.systems/) (another angle on...

I can imagine following someone and not wanting to notify them I am doing that. So I don't think point **1** user A being added to user B's following collection...

@evanp foaf also has a notion of groups. So you can have a number of different groups, such as those people you follow, those people who follow you, the members...

The question is wether we can come to some agreement ourselves when building apps to use similar vocabularies. I think at least having a table somewhere of vocabs used, and...