global definition

Stream: new members

[Georgi Kocharyan]

another post on word metric: So I have a file where I prove a bunch of stuff about the word metric on groups, and I'd like for every time I write "cayleydist g h" or something similar for Lean to know I mean the word metric (which I have defined)

noncomputable instance word_metric {G: Type*} [group G] [inhabited G] (S : set G)
 (hS : G = subgroup.closure S) : pseudo_metric_space G :=

This works fine within a theorem, I just say let cayleydist := (word_metric ...).dist. Can I somehow make this work over all of the defs and thms in my file?