Question: Comp.up carries an OpId := String. Source.step matches on string literals "raise", "get", "put". String-typed operation names lose type safety (no exhaustiveness check; typos compile).

Options:

1. Keep OpId = String. Pragmatic; user-extensible.
2. Symbolic enum: inductive OpId | raise | get | put | .... Type-safe but not extensible without modifying the kernel.
3. Per-effect operation namespacing: each Eff carries its own operation alphabet (similar to algebraic theory presentation).

Recommended: (1) for now. Revisit if proofs demand string-free operations.

Blocked on: nothing. Style/ergonomics question.

Revisit signal: cannot prove a property because it requires exhaustive case analysis on operation names.