Zulip Chat Archive

Stream: mathlib4

Topic: assert_not_exists


Scott Morrison (Dec 13 2022 at 21:40):

@Mario Carneiro, would you have a chance to update mathport for the new commands/tactics recently:

/- ./././Mathport/Syntax/Translate/Command.lean:719:14: unsupported user command assert_not_exists -/

Yaël Dillies (Feb 24 2024 at 15:39):

Could we make assert_not_exists say what path a forbidden is transitively imported through? Climbing up the imports copy-pasting the assert_not_exists is not really fun.

Kim Morrison (Feb 24 2024 at 21:32):

Yaël Dillies said:

Could we make assert_not_exists say what path a forbidden is transitively imported through? Climbing up the imports copy-pasting the assert_not_exists is not really fun.

That sounds a good idea. If anyone would like to implement this it is relatively easy metaprogramming, and there is code to cargo cult in the import-graph library and in the implementation of #find_home.

Mario Carneiro (Feb 24 2024 at 22:46):

#10940

Yaël Dillies (Mar 06 2024 at 11:44):

Thanks, it's very useful!


Last updated: May 02 2025 at 03:31 UTC