Coq のモジュールシステムについて，使い方がいまいちつかめてない気がしたので stdlib でどう使われてるのか見てみました。はじめに，モジュールとはどういうものかを一応言語化してみる。Coq の module はまあいわゆる module だと思っていればよいと思う…