Hiroki Tokunaga (Dec 06 2023 at 01:03): Hiroki Tokunaga (Dec 06 2023 at 01:03):Thank you all for your comments. I tried Pptactic.pr_alias_key (instead of Pptactic.pr_alias because it had a too complex type) and it seemed to work. At least I could distinguish symmetry in and info_auto with it.
I'm sure there'll always be some Coq code that my formatter can't format due to Coq's extension mechanism but will try developing it with AST because I did it in the same way in Haskell, and thus it's somewhat an easy way for me to format some amounts of Coq code.
Notification Bot (Dec 06 2023 at 01:03):Hiroki Tokunaga has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC