What should I do if I have need for the following? Does already exist 
any equivalent solution?

I'd like to write:

type subindex = int invariant x -> (x>=10)&&(x<=100)

let doit (a:subindex) (b:subindex) =
  let result = some_operation a b in
  (result:subindex)

And it should be translated to:

type subindex = int
let subindex_invariant x = (x>=10)&&(x<=100)

let doit (a:subindex) (b:subindex) =
  assert (subindex_invariant a);
  assert (subindex_invariant b);
  let result = some_operation a b in
  assert (subindex_invariant result);
  (result:subindex)

Am I going right direction at all?

----------------------------------------------------
Promocyjne oferty biletów lotniczych!
Praga, Rzym, Pary¿, Mediolan ju¿ od 499z³ - Kliknij:
http://klik.wp.pl/?adr=http%3A%2F%2Fsamoloty.wp.pl%2Fpromocje%2F&sid=202