Commit 2024-01-17 01:03 5919dba2

View on Github →

chore: bump Std to leanprover/std4#421 (#9798) This brings the new implementation of library_search to Mathlib. It is temporarily called std_exact? and std_apply?, but if it tests okay in Mathlib we will remove the old implementation. There is some change in the ordering of results, so please report on your experiences!

Estimated changes