Stream: Beginner Questions

Topic: Go-to-definition for fancy syntax

Jakub Kądziołka (Mar 19 2021 at 00:07):

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?

Jakub Kądziołka (Mar 19 2021 at 00:09):

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.

Manuel Eberl (Mar 19 2021 at 08:57):

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: Apr 23 2024 at 12:29 UTC