9ba41a692d
This PR implements better support for unfolding class fields marked as `reducible`. For example, we want to mark fields that are types such as ```lean MonadControlT.stM : Type u -> Type u ``` The motivation is similar to our heuristic that type definitions should be abbreviations. Now, suppose we want to unfold `stM m (ExceptT ε m) α` using the `.reducible` transparency setting, we want the result to be `stM m m (MonadControl.stM m (ExceptT ε m) α)` instead of `(instMonadControlTOfMonadControl m m (ExceptT ε m)).1 α`. The latter would defeat the intent of marking the field as reducible, since the instance `instMonadControlTOfMonadControl` is `[instance_reducible]` and the resulting term would be stuck when using `.reducible` transparency mode. **Remark**: This feature introduces a few breakages in core and Mathlib. So, it is disabled for now in this PR. To enable, we must use `set_option backward.whnf.reducibleClassField true` |
||
|---|---|---|
| .. | ||
| src | ||
| stdlib | ||