It seems that Lombardi and Quitté in their book "Commutative Algebra: Constructive Methods", Ch. XI, §3, define UFDs as GCD-domains such that every regular element is a product of irreducibles. In classical logic, this coincides with the usual definition. (Ingo sketched the proof in his comment.)
HeinrichD
- 5.5k
- 22
- 42