mathlib
938f1f1b - chore(tactic/core): fix bug in `resolve_attribute_expr_list` (#16827)

Commit
3 years ago
chore(tactic/core): fix bug in `resolve_attribute_expr_list` (#16827) See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/namespace.20affects.20behaviour.20of.20.60apply_list_expr.60 Co-authored-by: Alex J Best <alex.j.best@gmail.com> Co-authored-by: Alex J Best <alex.j.best@gmail.com>
Author
Parents
Loading