I've never used Rocq but from what I understand the core type theory is also a version of CIC and like Lean it has strong support for tactics. Rocq defaults to an axiom free core making it constructive. Classical axioms like propositional extensionality and axiom of choice are things you opt into deliberately.
From what I understand the Lean community leans (haha) classical and uses these axioms throughout mathlib. By staying constructive you guarantee that closed proofs can, in principle, evaluate to a canonical form.
From what I understand the Lean community leans (haha) classical and uses these axioms throughout mathlib. By staying constructive you guarantee that closed proofs can, in principle, evaluate to a canonical form.