Stream: Beginner Questions

Topic: shortcut


view this post on Zulip zibo yang (May 05 2021 at 16:17):

what is an efficient way or shortcut to find where something was defined? like I want to find definition of "map"

view this post on Zulip Manuel Eberl (May 05 2021 at 16:24):

Ctrl+click on it

view this post on Zulip Manuel Eberl (May 05 2021 at 16:24):

Anywhere where it appears in the inner syntax. e.g. when you do term "map"

view this post on Zulip Manuel Eberl (May 05 2021 at 16:25):

However, map is actually defined automatically by the datatype package during the definition of the list datatype. So all that will do is take you to that invocation of datatype.

view this post on Zulip Manuel Eberl (May 05 2021 at 16:25):

You could probably somehow get a hang of the actual definition, but that would be in terms of all kinds of internal stuff from the datatype package and not be very illuminating.


Last updated: Sep 25 2021 at 08:21 UTC