Zulip Chat Archive

Stream: general

Topic: tactic for unfolding definition


view this post on Zulip Kenny Lau (Mar 15 2018 at 19:56):

If I've defined def A := B and my goal / hypothesis contains A, how do I replace A with B?

view this post on Zulip Moses Schönfinkel (Mar 15 2018 at 19:58):

unfold :)

view this post on Zulip Kenny Lau (Mar 15 2018 at 19:58):

I tried it already

view this post on Zulip Kenny Lau (Mar 15 2018 at 19:59):

here's the context that might help: I'm defining A in the middle of a structure

view this post on Zulip Kenny Lau (Mar 15 2018 at 19:59):

class foo :=
(A := B)

view this post on Zulip Simon Hudon (Mar 15 2018 at 19:59):

What happens when you try it?

view this post on Zulip Kenny Lau (Mar 15 2018 at 20:00):

unfold tactic failed, A does not have equational lemmas nor is a projection

view this post on Zulip Moses Schönfinkel (Mar 15 2018 at 20:00):

ok first let's eliminate one problem; try delta instead of unfold

view this post on Zulip Moses Schönfinkel (Mar 15 2018 at 20:00):

if that works, you're trying to unfold something you have no "business" unfolding

view this post on Zulip Kenny Lau (Mar 15 2018 at 20:00):

dsimplify tactic failed to simplify

view this post on Zulip Reid Barton (Mar 15 2018 at 20:02):

isn't (A := B) there just a default value?

view this post on Zulip Kenny Lau (Mar 15 2018 at 20:02):

oh... I can't define things inside a structure?

view this post on Zulip Simon Hudon (Mar 15 2018 at 20:03):

No, that's not possible

view this post on Zulip Kenny Lau (Mar 15 2018 at 20:04):

ok

view this post on Zulip Simon Hudon (Mar 15 2018 at 20:04):

That would be useful

view this post on Zulip Simon Hudon (Mar 15 2018 at 20:04):

They might consider it in the future. Recently, they have adopted implicit fields

view this post on Zulip Reid Barton (Mar 15 2018 at 20:06):

You can sort of emulate it with multiple structures, like how the algebraic classes are build on top of has_foo classes and so can take advantage of intervening notation declarations


Last updated: May 13 2021 at 06:15 UTC