Commit 2020-10-29 22:37 fc307f9b

feat(tactic/norm_num): make norm_num extensible (#4820) This allows you to extend norm_num by defining additional tactics of type expr → tactic (expr × expr) with the @[norm_num] attribute. It still requires some tactic proficiency to use correctly, but it at least allows us to move all the possible norm_num extensions to their own files instead of the current dependency cycle problem. This could potentially become a performance problem if too many things are marked @[norm_num], as they are simply looked through in linear order. It could be improved by having extensions register a finite set of constants that they wish to evaluate, and dispatch to the right extension tactic using a name_map.

def foo : ℕ := 1
@[norm_num] meta def eval_foo : expr → tactic (expr × expr)
| `(foo) := pure (`(1:ℕ), `(eq.refl 1))
| _ := tactic.failed
example : foo = 1 := by norm_num