18 lines
443 B
Text
18 lines
443 B
Text
|
let splitAndCompare
|
||
|
|
: ∀(a : Type) →
|
||
|
|
(a → Bool) →
|
||
|
|
(a → a → Integer) →
|
||
|
|
(a → a → Integer) →
|
||
|
|
a →
|
||
|
|
a →
|
||
|
|
Integer
|
||
|
|
= λ(t : Type) →
|
||
|
|
λ(p : t → Bool) →
|
||
|
|
λ(yes : t → t → Integer) →
|
||
|
|
λ(no : t → t → Integer) →
|
||
|
|
λ(a : t) →
|
||
|
|
λ(b : t) →
|
||
|
|
if p a then if p b then yes a b else -1 else if p b then +1 else no a b
|
||
|
|
|
||
|
|
in splitAndCompare
|