You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
A reference catalog of all macro_rules! macros in the elicitation workspace.
Proc-derive macros live in elicitation_derive; the macros below are all
declarative (macro_rules!) and are exported from their respective crates.
elicitation crate
Newtype macros — src/newtype_macro.rs
Macro
Purpose
elicit_newtype!
Core newtype generator. Wraps a foreign type with a named struct, derives ElicitComplete, Prompt, Elicitation, KaniCompose, ElicitSpec, ElicitPromptTree, and all formal-verification proof hooks.
elicit_newtype_traits!
Adds supplemental trait impls to an already-declared newtype (Display, From, Into, etc.).
elicit_newtype_trait_flag!
Adds a single marker-trait impl to a newtype (used for opt-in trait flags).
elicit_newtypes!
Batch convenience: calls elicit_newtype! repeatedly for a list of types.
Generates an ElicitComplete shadow enum that mirrors a foreign enum, adding From/Into conversions, elicitation dispatch, and formal-verification hooks.
select_trenchcoat_traits!
Adds supplemental trait impls to a trenchcoat enum.
Emit / plugin registration — src/emit_code.rs
Macro
Purpose
register_emit!
Registers an emission handler (a plugin's emit() impl) into the global plugin registry. Called once per plugin in the plugin's module.
Styling — src/default_style.rs
Macro
Purpose
default_style!
Generates a single-variant unit enum that implements ElicitationStyle, used to declare the default UI style for a primitive type.
Contracts — src/contracts.rs
Macro
Purpose
proof_credential!
Declares a named proof-credential type (struct MyCredential;) and registers it with the ProvableFrom lattice.
kani_label!
Attaches a human-readable label and metadata to a Kani proof harness for documentation and tooling.
elicit_accesskit crate
src/lib.rs
Macro
Purpose
accesskit_copy_enum!
Generates an elicitation-compatible shadow of an AccessKit enum, preserving variant names and adding From/Into, Serialize/Deserialize, JsonSchema, and Elicit impls.
elicitation_kani crate
src/harness_helpers.rs
Helper utilities and the kani_arbitrary! macro for writing Kani proof
harnesses for types with String or Vec<T> fields that Kani cannot derive
Arbitrary for natively.
Item
Kind
Purpose
bounded_string::<N>()
#[cfg(kani)] fn
Generate an N-byte arbitrary String.
bounded_option_string::<N>()
#[cfg(kani)] fn
Generate None or an N-byte arbitrary String.
bounded_vec::<T, N>()
#[cfg(kani)] fn
Generate a Vec<T> with 0..N arbitrary elements.
kani_arbitrary!
macro_rules!
Emit a kani::Arbitrary impl that uses the bounded helpers above.
Internal (non-exported) macros
Many crates contain macro_rules! helpers that are not#[macro_export]
and are only visible within their defining module. They are intentionally
omitted from this catalog; consult the source files directly.