Lean 4 tips ： main関数とライブラリサーチ

def main (args : List String) : IO UInt32 := do

import Mathlib.Tactic.LibrarySearch
#check library_search%

パーセント記号は相変わらず意味不明。