search

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
194 stars 49 forks source link

Rename may_diverge, must_diverge, BoxFinite, DiamondFinite to (all|any)_(in|)finite and EuttDiv -> EuttNoRet #239

Closed Lysxia closed 2 years ago

Lysxia commented 2 years ago

IMO divergence ⌿ infinity. "divergence" would better describe unresponsive trees, i.e., spin and those that throw exceptions.