What we need is a numeric type that cannot be zero.
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
alt Hacker News
What we need are refinement types, where there’s a base type and a predicate. F* has this: