定義 definitionとaxiomatization

definition はPureレベルで使える。definitionは定数定義、関数定義に使えるが、形式としては、等号的公理の追加になる。"左辺 == 右辺" で、「右辺により左辺が定義される」と読むようだ。左辺は定数、関数・演算子の呼び出し形式とか。書き換え規則を定義するようだ、たぶん。

axiomatization/whereとdefinition/whereの使い分けがワカラン。

ところで、axiomatization/whereは、where部だけ、つまり公理による制約だけでも書ける。whereの前にシグネチャを書くが、シグネチャは不要で、それ以前に定義された（登録された）記号は自由に使える。よって、単一の定義を幾つかのaxiomatization宣言に分けて書ける。