Derive Lazy unfolding hints

Available from bluerock.auto.elpi.derive.lazy_unfold.

This command does not yet support usages inside Sections.

Usages

#[only(lazy_unfold(locality)] derive R. where locality ∈ { global, local, export }
#[only(lazy_unfold)] derive R. is the same as #[only(lazy_unfold(export))] R.

The command defines and registers lazy unfolding hints for R.

For example,

Definition R `{Σ : cpp_logic} {σ : genv} (q : cQp.t) : Rep := Rbody q.
#[only(lazy_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.