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 theassert_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):
Yaël Dillies (Mar 06 2024 at 11:44):
Thanks, it's very useful!
Last updated: May 02 2025 at 03:31 UTC