environはエキスパートでないと書けない

environは地獄だ。environはノービスには書けない。エキスパートが書いてあげるのが前提みたいだ。

スライド http://mizar.org/cicm_tutorial/mizar.pdf "Mizar Hands-on Tutorial" by Adam Naumowicz, Artur Korni lowicz, Adam Grabowski (July 29, 2016) の45ページにあったのコードは、"Exemplary scheme proof (special student environment)"となる。special student environmentは学生の学習用に作った環境部のことだろう。

また、http://www.cs.shinshu-u.ac.jp/~okazaki/TPP2012shidama.pdf 「日本における Mizar プロジェクトの現状と展望」 師玉康成 (2012.11.21) によると、environ部は学習者には書かせないようである。

証明文の冒頭に環境部と呼ばれる証明中で用いられる単語の定義やすでに証明済みの定理を参照するためのライブラリ名を記述するが，学習者にとってはこれらのライブラリの検索に時間を取られ肝心の証明文の記述に労力を費やすことができないことを回避するためであり，環境部や証明の骨子部分を教師が用意し学習者は必要な個所のみ思考すればよいこととしている．