Lean 4 tips ： main関数、ライブラリサーチ、名前短縮

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

import Mathlib.Tactic.LibrarySearch
#check library_search%

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

名前短縮とは、修飾名を短くすること。ひとつは、open でカレント名前空間に別名前空間の名前をぶちまける。もうひとつの方法は当該名前空間に入って（namespace宣言して）、そこで名前を使う。