Commit 2026-02-28 12:29 4f48d80b

View on Github →

fix: provide #min_imports and other commands in Mathlib.Init (#35143) Make these commands available across Mathlib:

  • #help
  • #min_imports
  • #min_imports in
  • #find_home
  • proof_wanted Add tests that verify commands work when importing basic files, to prevent regressions.

Estimated changes

added theorem test_lemma
added theorem test_type_star
added theorem test_check_tactic
added theorem test_count_heartbeats
added theorem test_print_sorries
added theorem test_whatsnew