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?