441b9077b2
We need this procedure otherwise it takes forever to prove equation lemmas for definitions such as: ``` def macros : name → option macro | `lambda := some lambda_macro | `intro_x := some intro_x_macro | _ := none ``` We never experienced this problem in Lean3 because we used `name` literals only occurred in patterns of *meta* definitions. So, no equation lemma was generated. @kha `def macros` was taking more than 1 second to elaborate on my machine. It is now instantaneous. |
||
|---|---|---|
| .. | ||
| core | ||
| ir | ||
| parser | ||
| config.lean | ||
| disjoint_set.lean | ||
| format.lean | ||
| level.lean | ||
| macro.lean | ||
| name.lean | ||
| name_mangling.lean | ||
| options.lean | ||
| pos.lean | ||
| trace.lean | ||