forget some declaration

Stream: Is there code for X?

[Huajian Xin]

Is there any method to make the Lean Checker forget some declarations made before?

[Henrik Böving]

At least none that I've ever seen used. What are you actually trying to achieve? This sounds like #xy

[Shreyas Srinivas]

Huajian Xin said:

Is there any method to make the Lean Checker forget some declarations made before?

If you want to hide some names from the rest of your code, putting them inside sections or namespaces is the way to go as far as I know

[Martin Dvořák]

If you are inside a tactic-style proof, you can use clear to forget stuff declared above.

[Yaël Dillies]

or tactic#clear_dependent if tactic#clear doesn't cut it

[Patrick Johnson]

Huajian Xin said:

Is there any method to make the Lean Checker forget some declarations made before?

If your declaration represents a model of an abstract structure and after you create an API to work with it you want to forget the explicit model, then you can use constant (in Lean 4), or classical epsilon in Lean 3 (also in Lean 4).

[Henrik Böving]

It's opaque instead of constant.