Commit 2022-08-06 10:05 28a4767d

feat: norm_num1 (#326) todos:

• implement norm_num at a local hypothesis how should I do this?
• norm_num as a simp-like tactic? i.e; eg norm num at ⊢ isPrime (x + (2 + 3)) should give ⊢ isPrime (x + 5)?
• port examples and tests
• original norm_num uses simp with discharger being norm_num again.