blob: ec48523009aa3a971d544538fa3393b2b9ecd71b (
plain)
1
2
3
4
5
6
7
8
9
10
|
Parameter compare : forall n m : nat, {n < m} + {n = m} + {n > m}.
Type
match compare 0 0 return nat with
(* k<i *) | left _ (left _ _) => 0
(* k=i *) | left _ _ => 0
(* k>i *) | right _ _ => 0
end.
end.
|