Commit 2022-11-07 21:34 a300eb9d

feat: #conv command: #simp, #norm_num etc. (#539) The command #conv $tac => $e will run a conv tactic tac on e and display the resulting simplified version of e'. This is used to implement several other user commands:

• #whnf e displays the weak head normal form of e
• #simp e displays the simp normal form of e
• #norm_num e evaluates e using norm_num
• #push_neg e shows the result of push_neg on e The conv versions of norm_num and push_neg are also added here, so that the commands can be implemented as macros.