EvalML1Errにおける評価の全域性の証明でML1*1のすべての式に評価される値が存在することが分かったので、式を評価する関数書いてみたいと思います。また、せっかくCoqで書いたので関数が妥当であるかの証明とOCamlソースコードの出力も行おうと思います。 *…