What is the `Backtrackable` type class used for?

Stream: general

[Derrik Petrin]

From what I can tell, this type class only appears in Prelude.lean, and no structures are actually ever registered as instances of the class, in lean4 or in mathlib. The MonadBacktrack class seems to be completely independent machinery.

[Niels Voss]

Do you mean the EStateM.Backtrackable? I know it is at least used in EStateM.tryCatch and EStateM.orElse but the only instance of it is the dummy default instance EStateM.nonBacktrackable

[Niels Voss]

It seems that for any T, we could define an instance EStateM.Backtrackable T T quite easily, but maybe that isn't done for performance reasons, or because it would break IO by causing time-travelling IO.RealWorld tokens

[Derrik Petrin]

Yes, sorry, I meant EStateM.Backtrackable. I wonder if this was something implemented with the idea that it would be used at some point in the future, but that never happened?

[Derrik Petrin]

What you describe is what I understood from the code as well.

[David Thrane Christiansen]

It's described in this section of the language reference

[Eric Wieser]

Is EStateM supposed to be a lean implementation detail, or is it fair game for user code?

[David Thrane Christiansen]

Fair game for use code :)

[Eric Wieser]

Excellent, that makes lean4#3010 a little more justifiable then :)