mathlib
0e93816c - feat(tactic/norm_num_command): add user command to run norm_num on an expression (#12550)

Commit

3 years ago

feat(tactic/norm_num_command): add user command to run norm_num on an expression (#12550) For example, ``` #norm_num 2^100 % 10 -- 6 ```

Author

kmill

Parents