structure Lean.Meta.Sym.BackwardRule : Type

A rule for backward chaining (goal transformation).

Given a goal ... ⊢ T, applying a BackwardRule derived from a theorem ∀ xs, P will unify T with P, assign the goal to the theorem application, and return new goals for the unassigned arguments in xs.

• expr : Expr

  The theorem used to create the rule. It is often of the form Expr.const declName.

• pattern : Pattern

  Precomputed pattern for efficient unification.

• resultPos : List Nat

  Indices of arguments that become new subgoals, ordered with non-dependent goals first.

def Lean.Meta.Sym.mkBackwardRuleFromDecl (declName : Name) (num? : Option Nat := none) : MetaM BackwardRule

Creates a BackwardRule from a declaration name.

The num? parameter optionally limits how many arguments are included in the pattern (useful for partially applying theorems).

Equations

• One or more equations did not get rendered due to their size.

inductive Lean.Meta.Sym.ApplyResult : Type

• failed : ApplyResult
• goals (mvarIds : List MVarId) : ApplyResult

def Lean.Meta.Sym.BackwardRule.apply (mvarId : MVarId) (rule : BackwardRule) : SymM ApplyResult

Applies a backward rule to a goal, returning new subgoals.

1. Unifies the goal type with the rule's pattern
2. Assigns the goal metavariable to the theorem application
3. Returns new goals for unassigned arguments (per resultPos)

Returns .notApplicable if unification fails.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Sym.BackwardRule.apply' (mvarId : MVarId) (rule : BackwardRule) : SymM (List MVarId)

Similar to `BackwardRule.apply', but throws an error if unification fails.

Equations

• One or more equations did not get rendered due to their size.