Commit 2020-10-11 20:09 952a407c
View on Github →feat(data/nat/digits): add norm_digits tactic (#4452)
This adds a basic tactic for normalizing expressions of the form nat.digits a b = l. As requested on Zulip: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/simplifying.20nat.2Edigits/near/212152395