Agdaの証明と論文

まぁ、論文ってほどでもなかったりするんだが、なんと3月からはまっている Zorn の補題の証明をプロシンに出すんですが、

　　まだ、Agdaの方が終わってない

まぁ、間に合うはずなんですが。良くあることなんだが、

　　論文書き始めると整理されるので見通しが良くなる

なので、もっと早く書けば良かった。いろいろ原因はあるんだが、

　　色々細かい選択肢があるが、それのどこがだめだったか忘れて振動する
　　Agda は「とにかく、そこにある記号で穴を埋める」ってのがあって、それに引きづられる

ってのがあるのだけど、文章にするとそれが整理されるらしい。

でも、まぁ、証明は一応つながって「実はあれもこれも不要で小さくなりそう」みたいな段階ではある。

ところが、そこから「やっぱりうまくいかん」ってのを繰り返してたりするんだよな。まぁ、数学者なら

　　Zorn の補題? あんなの簡単じゃん

であろうとは思います。

LuaLaTeX なんだが、STIX font で ⟪ ⟫ がでなくてちょっと困ってます。なんでだ。