Unfolding opaque definitions

Stream: new members

[Robert Maxton]

Please tell me there's a better way than this:

unfold has_lt.lt preorder.lt partial_order.lt linear_order.lt at tri

[Robert Maxton]

dsimp fails to simplify, so does norm_cast

[Yaël Dillies]

You can use change (docs#tactic.interactive.change)

[Yaël Dillies]

But with more context we coul probably give you a better solution.

[Robert Maxton]

nah, change was basically what I wanted in this case
in general it'd be cool if I could just unfold "everything with a field syntax" but that might have problems in the general case

[Eric Rodriguez]

change is brittle, it's usually nicer to have a ..._def lemma

[Eric Wieser]

Usually this means you should write a lemma with a proof of rfl to do the unfolding for you

[Kyle Miller]

@Robert Maxton I think tactic#unfold_proj might be what you're looking for (whether or not it might be the "right" thing to do).

[Robert Maxton]

indeed it is. it's a little overenthusiastic but I can hardly complain

[Robert Maxton]

thanks :p

[Kyle Miller]

It has some configuration options (same ones as dsimp), so for example unfold_projs at h {single_pass := tt}. With this you could do iterate 3 { unfold_projs at h {single_pass := tt} } for instance.