Passing informations to fun_prop

Stream: mathlib4

[Etienne Marion]

When fun_prop fails, it can sometimes tell you where it failed, and which assumption was missing. You can then make it work by writing fun_prop (disch := tactic), where tactic solves the issue. Do you think it might be possible to implement a fun_prop [h1, h2] syntax to tell fun_prop it can use h1 and h2 to discharge side conditions? This would be more convenient I think. I do not know anything about meta-programming though so maybe it's quite complicated.

[Aaron Liu]

What's the default discharger?

[Aaron Liu]

It looks like the default discharger is to just fail :(

[Aaron Liu]

We could make it something cheap like solve_by_elim

[Aaron Liu]

Then fun_prop [h1, h2] could just be have := h1; have := h2; fun_prop and then solve_by_elim will capture it

[Etienne Marion]

Well I gotta say that does not seem much more convenient to me.

[Aaron Liu]

What is not more convenient?

[Etienne Marion]

Having to introduce the hypotheses in haves before hand does not seem more convenient than specifying the discharger.

[Aaron Liu]

No, I mean if solve_by_elim is the default discharger then fun_prop [h1, h2] could be a macro or something that expands to have := h1; have := h2; fun_prop

[Etienne Marion]

Oh sorry I misunderstood! Yes that would be great.