mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: norm_num extensions

Open digama0 opened this issue 3 years ago • 1 comments
trafficstars

This PR is an almost complete rewrite of norm_num to implement its functionality via an extensible attribute for plugins, and use Qq for expression construction.

digama0 avatar Oct 13 '22 06:10 digama0

This is really nice, and helpful for me to understand how to use QQ!

I added doc-strings to nearly all the defs. Feel free to discard if you don't like them.

kim-em avatar Oct 13 '22 08:10 kim-em

bors merge

kim-em avatar Oct 20 '22 03:10 kim-em

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Oct 20 '22 03:10 bors[bot]