assert_not_exists

Stream: mathlib4

[Scott Morrison]

@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]

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]

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]

#10940

[Yaël Dillies]

Thanks, it's very useful!