Zulip Chat Archive

Stream: new members

Topic: unfold a symbol


view this post on Zulip Patrick Lutz (May 26 2020 at 20:32):

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

view this post on Zulip Johan Commelin (May 26 2020 at 20:33):

dsimp [has_le.le]

view this post on Zulip Johan Commelin (May 26 2020 at 20:33):

Or dsimp [(≤)]

view this post on Zulip Patrick Lutz (May 26 2020 at 20:33):

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

view this post on Zulip Johan Commelin (May 26 2020 at 20:34):

I don't know...

view this post on Zulip 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).

view this post on Zulip 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)

view this post on Zulip Pedro Minicz (May 26 2020 at 20:43):

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

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 26 2020 at 20:57):

Yes, this is what I call debugging

view this post on Zulip 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