Commit 2023-08-27 05:46 49a849ef

feat: fix norm num with arguments (#6600) norm_num was passing the wrong syntax node to elabSimpArgs when elaborating, which essentially had the effect of ignoring all arguments it was passed, i.e. norm_num [add_comm] would not try to commute addition in the simp step. The fix itself is very simple (though not obvious to debug!), probably using TSyntax more would help avoid such issues in future. Due to this bug many norm_num [blah] became rw [blah]; norm_num or similar, sometimes with porting notes, sometimes not, we fix these porting notes and other regressions during the port also. Interestingly cancel_denoms uses norm_num [<- mul_assoc] internally, so cancel_denoms also got stronger with this change.