| 1050.lean:7:2-18:5: error: invalid mutual definition, result types must be in the same universe level, resulting type for `Foo.bar` is | |
| Foo as bs → bs : Type (u + 1) | |
| and for `Foo.bar_aux` is | |
| bs : Type u | |
| 1050.lean:24:8-24:12: warning: declaration uses 'sorry' | |
| 1050.lean:24:8-24:12: warning: declaration uses 'sorry' |