これはアルゴリズムです： // Precondition: n > 0
l = -1;
r = n;
while (l+1 != r) {
m = (l+r)/2;
// I && m == (l+r)/2
if (a[m] <= x) {
l = m;
} else {
r = m;
}
}
// Pos
私はこのうち(x < y)の証明を抽出するにはどうすればよい IsLt : Ord a => (x: a) -> (y: a) -> Type
IsLt x y = So (x < y)
のようなものが作成したSo (x < y)ようSoタイプを、持っている場合は？私はこれのための標準ライブラリで関数を見つけることができません。 Soは、次のように標準ライブラリで定義されています data