This PR makes `@[cbv_opaque]` unconditionally block all evaluation of a
constant
by `cbv`, including `@[cbv_eval]` rewrite rules. Previously,
`@[cbv_eval]` could
bypass `@[cbv_opaque]`, and for bare constants (not applications),
`isOpaqueConst`
could fall through to `handleConst` which would unfold the definition
body.
The intended usage pattern is now: mark subterm-producing functions
(like
`DHashMap.insert`) as `@[cbv_opaque]` to prevent unfolding, and provide
`@[cbv_eval]` theorems on the *consuming* function (like
`DHashMap.contains`)
which pattern-matches against the opaque subterms.
This PR adds the ability to register theorems with the `cbv_eval`
attribute in the reverse direction using the `←` modifier, mirroring the
existing `simp` attribute behavior. When `@[cbv_eval ←]` is used, the
equation `lhs = rhs` is inverted to `rhs = lhs`, allowing `cbv` to
rewrite occurrences of `rhs` to `lhs`.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
