mathlib
69be6fe3 - fix(tactic/monotonicity/interactive): fix the order of calling `unify_with_instance` (#16480)

Commit
3 years ago
fix(tactic/monotonicity/interactive): fix the order of calling `unify_with_instance` (#16480) [Zulip](https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/.60apply_instance.60.20fails.20to.20infer.20instance.3F)
Author
Parents
Loading