Derive Eager unfolding hints

Available from bluerock.auto.elpi.derive.eager_unfold.

This command does not yet support usages inside Sections.

Usages: #[only(eager_unfold)] derive R.

The command defines and registers hints that eagerly unfold/unlock predicates. These hints have locality export.

For example

Definition R `{Σ : cpp_logic} {σ : genv} q : Rep := Rbody q.
#[only(eager_unfold)] derive R.

registers a (exported) hint of the form ∀ q, R q -|- Rbody q that will only trigger when the goal contains Rbody q.