tactic for unfolding definition

Stream: general

[Kenny Lau]

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

[Moses Schönfinkel]

unfold :)

[Kenny Lau]

I tried it already

[Kenny Lau]

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

[Kenny Lau]

class foo :=
(A := B)

[Simon Hudon]

What happens when you try it?

[Kenny Lau]

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

[Moses Schönfinkel]

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

[Moses Schönfinkel]

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

[Kenny Lau]

dsimplify tactic failed to simplify

[Reid Barton]

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

[Kenny Lau]

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

[Simon Hudon]

No, that's not possible

[Kenny Lau]

ok

[Simon Hudon]

That would be useful

[Simon Hudon]

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

[Reid Barton]

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