Stream: Coq users

Topic: Renaming a Definition/Lemma


view this post on Zulip Arnoud van der Leer (Feb 06 2024 at 07:21):

The UniMath library has, in it's 16 years of existence, acquired a lot of code in a lot of different styles. Suppose one wants to update file / definition / lemma names. Is there a tool (more intelligent than find-replace) that can update references? (like imports and qualifiers for files, and just the name for lemmas and defs?)

view this post on Zulip Li-yao (Feb 06 2024 at 09:15):

I don't know if something like that exists already but it seems quite feasible using the .glob files generated during compilation.

view this post on Zulip Arnoud van der Leer (Feb 15 2024 at 13:18):

For future me's: I threw something together using python.

view this post on Zulip walker (Feb 15 2024 at 13:51):

that is cool! it will be nice if one day we end up having coq linter or formatting tool that one can contribute to (cannot be another ocaml project by definition)!

view this post on Zulip Arnoud van der Leer (Feb 15 2024 at 13:52):

Thank you!
It is very ramshackle, but on the fairly large UniMath library it worked (almost) fine ^^


Last updated: Jun 23 2024 at 05:02 UTC