Zulip Chat Archive

Stream: new members

Topic: global definition

Georgi Kocharyan (Jul 20 2022 at 14:43):

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?

Last updated: Dec 20 2023 at 11:08 UTC