## Stream: general

### Topic: tactic for unfolding definition

#### 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?

#### Moses Schönfinkel (Mar 15 2018 at 19:58):

unfold :)

#### 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

#### Kenny Lau (Mar 15 2018 at 19:59):

class foo :=
(A := B)


#### Simon Hudon (Mar 15 2018 at 19:59):

What happens when you try it?

#### Kenny Lau (Mar 15 2018 at 20:00):

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


#### Moses Schönfinkel (Mar 15 2018 at 20:00):

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

#### Moses Schönfinkel (Mar 15 2018 at 20:00):

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

#### Kenny Lau (Mar 15 2018 at 20:00):

dsimplify tactic failed to simplify


#### Reid Barton (Mar 15 2018 at 20:02):

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

#### Kenny Lau (Mar 15 2018 at 20:02):

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

#### Simon Hudon (Mar 15 2018 at 20:03):

No, that's not possible

ok

#### Simon Hudon (Mar 15 2018 at 20:04):

That would be useful

#### Simon Hudon (Mar 15 2018 at 20:04):

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

#### 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