I have encountered the syntax `∑x∈#?A. ?f x`

. Unlike simple infix operators or plain constant names, ctrl+clicking on this does not show me the definition of the relevant constant. How can I see the definition for more complex syntax?

In this case, some strategic grepping of HOL-Library allowed me to find

```
"∑i ∈# A. b" ⇌ "CONST sum_mset (CONST image_mset (λi. b) A)"
```

However, I'd still like to know a general solution.

Quick hack: `ML_val ‹@{term "∑i∈#A. b"}›`

That gives you the following output:

```
val it =
Const ("Multiset.comm_monoid_add_class.sum_mset", "'a multiset ⇒ 'a") $
(Const ("Multiset.image_mset", "('b ⇒ 'a) ⇒ 'b multiset ⇒ 'a multiset") $
Abs ("i", "'b", Free ("b", "'a")) $ Free ("A", "'b multiset")):
term
```

Last updated: Sep 25 2022 at 23:25 UTC