unfold a symbol

Stream: new members

[Patrick Lutz]

How do you unfold the definition of a symbol like $\leq$?

[Johan Commelin]

dsimp [has_le.le]

[Johan Commelin]

Or dsimp [(≤)]

[Patrick Lutz]

Is there any reason that unfold doesn't work for this?

[Johan Commelin]

I don't know...

[Pedro Minicz]

Could you show in which situation unfold has_le.leisn't working for you? It seems to work fine for me (in a weird way, unfolding a ≤ b to the unintuitive a.le b).

[Patrick Lutz]

@Pedro Minicz that works, but I meant why I can't do something like unfold \leq or unfold (\leq)

[Pedro Minicz]

I see, being able to unfold (\le) would be nice.

[Patrick Massot]

This is well known to be inconvenient. But also well-known to be a bad idea in the first place (although it's sometimes tempting for debuging purposes).

[Patrick Lutz]

@Patrick Massot Why is it a bad idea? It seems convenient to me to be able to unfold things if you forget how exactly they are defined (and then to delete the unfold once you see). Is that bad?

[Patrick Massot]

Yes, this is what I call debugging

[Patrick Lutz]

Oh, I see. I think I normally only use debugging to mean when I've already written some code and there are problems, so I got confused