忘れたので、素朴な疑問からやり直す

しばらく触ってないとテキメンに忘れる。

• Require ってどう使う？ Require Import/Exportって何？
• Class定義構文、Class Foo : Bar のBarってどう使う？
• Notationのスコープってどうやって使う？
• スコープバインドは、Bind Scope hoge_scope with Hoge. みたいに使うらしいが。
• Arguments の意味と使い方。

一生懸命にいじっていたときにこまめにメモしておけば良かったと後悔。