The term-creation specification

One op% entry per term kind, written in the typed form, split by theory. Nothing is generated here: entries are registered in opSpecExt and consumed by gen_untyped%/gen_typed% in the per-theory modules under Cvc/Untyped/ and Cvc/Typed/.

Spec/Defs.lean holds the data — shapes, sizes, notations, OpSpec and the extension — and Spec/Decl.lean the op% command that populates it. Everything else in this directory is specification, one module per theory.

This root aggregates them for convenience. A generation site imports only the theory it generates, which is what keeps a consumer from compiling specifications it never uses.