def main (args : List String) : IO UInt32 := doimport Mathlib.Tactic.LibrarySearch #check library_search%パーセント記号は相変わらず意味不明。

http://www.omdoc.org/pubs/omdoc1.2.pdf の印刷ページ21（p.37）から：Definition 3.2.5 (Monoid) A monoid is a semigroup $`S = (G, \circ)`$ with an element $`e\in G`$, such that $`e ◦ x = x`$ for all $`x ∈ G`$. $`e`$ is called a left unit of $…