Commit 2026-03-21 05:43 080afd21
View on Github →chore: import Type* in Mathlib.Init (#36316)
The implementation of Type* is very short, so I've put its minimal dependencies in the same file, Mathlib.Tactic.TypeStar, and imported this in Mathlib.Init. This allows us to get rid of many explicit imports of this file, and lets it be available everywhere in mathlib.