deciding if `refl` would work

Stream: general

[Scott Morrison]

I have lhs rhs : expr, and I would like to know, if the goal were to be lhs = rhs, whether or not refl would succeed. I could temporarily make the goal actually lhs = rhs, and try refl, but I'm wondering if it can be done directly.

[Scott Morrison]

I'm only hesitant to overwrite the goal because the actual current goal may be something completely unrelated to what my tactic is thinking about that the moment it's wondering about lhs = rhs, and it feels kludgy to actually have to use set_goal.

[Scott Morrison]

The problem is that refl is basically just shorthand for mk_const `eq.refl >>= λ r, apply_core r, and apply_core only unifies with the goal.

[Sebastian Ullrich]

@Scott Morrison Take a look at tactic.solve_aux

[Scott Morrison]

Thanks @Sebastian Ullrich. Implicit in your answer is "get over it, just set_goal to whatever you want, it's how you're meant to do this"! Good to know.

[Sebastian Ullrich]

If you want to look at it like that, yes :)

[Simon Hudon]

What if you try to unify them directly? unify lhs rhs