In the $F\star$ tutorial it says

Dv, the effect of a computation that may diverge;

what does diverge mean here? It's not explained and it confuses me.

I guess it means the type consists but the value varies, but if so why there isn't a non-diverge non-terminate effect?


1 Answer 1


In the theory of computation "diverge" means "does not terminate" or "runs forever". This is a computational effect (of a peculiar kind).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.