Type Alias ExprSubstitution 

pub type ExprSubstitution = HashMap<String, ProofExpr>;

Substitution for expression-level meta-variables (holes).

Maps hole names to their solutions, typically lambda abstractions inferred during higher-order pattern unification.

Example

Solving ?P(x) = Even(x) yields:

{ "P" ↦ Lambda { variable: "x", body: Even(x) } }

See Also

• unify_pattern - Creates expression substitutions via Miller pattern unification

Aliased Type

pub struct ExprSubstitution { /* private fields */ }