Theorem test_type_star

Modification history

2026-03-21 05:43

MathlibTest/BasicFiles/Init.lean

chore: import `Type*` in `Mathlib.Init` (#36316) …

Modified test_type_star View on Github →

2026-02-28 12:29

MathlibTest/BasicFiles/TacticBasic.lean

fix: provide `#min_imports` and other commands in `Mathlib.Init` (#35143) …

Added test_type_star View on Github →