zibo yang (May 05 2021 at 16:17): 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"
Manuel Eberl (May 05 2021 at 16:24):Ctrl+click on it
Manuel Eberl (May 05 2021 at 16:24):Anywhere where it appears in the inner syntax. e.g. when you do term "map"
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.
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: Apr 19 2024 at 20:15 UTC