What does `Dv` mean in $F\star$ language? 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?
In the theory of computation "diverge" means "does not terminate" or "runs forever". This is a computational effect (of a peculiar kind).