5.10 Description Operators HOLには二つの記述演算子があります。確定記述はその式を満たす唯一の値を表わします。不確定記述はその式を満たす任意の値を表わします。 5.10.1 Definite Description 確定記述は伝統的にιx. P(x)と書きます。これは、P(x)を満…