What we need are refinement types, where there’s a base type and a predicate. F* has this:

     val (/) : int -> (divisor:int { divisor <> 0 }) -> int