5 ms·
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
by drdaeman 22d ago
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