## Stream: new members

### Topic: unfold a symbol

#### Patrick Lutz (May 26 2020 at 20:32):

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

#### Johan Commelin (May 26 2020 at 20:33):

dsimp [has_le.le]

#### Johan Commelin (May 26 2020 at 20:33):

Or dsimp [(≤)]

#### Patrick Lutz (May 26 2020 at 20:33):

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

I don't know...

#### Pedro Minicz (May 26 2020 at 20:36):

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 (May 26 2020 at 20:41):

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

#### Pedro Minicz (May 26 2020 at 20:43):

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

#### Patrick Massot (May 26 2020 at 20:47):

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 (May 26 2020 at 20:52):

@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 (May 26 2020 at 20:57):

Yes, this is what I call debugging

#### Patrick Lutz (May 26 2020 at 20:58):

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

Last updated: May 12 2021 at 23:13 UTC