# Documentation

## Aesop.RulePattern

A rule pattern. For a rule of type ∀ (x₀ : T₀) ... (xₙ : Tₙ), U, a valid rule pattern is an expression p such that x₀ : T₁, ..., xₙ : Tₙ ⊢ p : P. Let y₀, ..., yₖ be those variables xᵢ on which p depends. When p matches an expression e, this means that e is defeq to p (where each yᵢ is replaced with a metavariable) and we obtain a substitution

{y₀ ↦ t₀ : T₀, y₁ ↦ t₁ : T₁[x₀ := t₀], ...}


Now suppose we want to match the above rule type against a type V (where V is the target for an apply-like rule and a hypothesis type for a forward-like rule). To that end, we take U and replace each xᵢ where xᵢ = yⱼ with tⱼ and each xᵢ with xᵢ ≠ yⱼ ∀ j with a metavariable. The resulting expression U' is then matched against V.

• An expression of the form λ y₀ ... yₖ, p representing the pattern.

• argMap :

A partial map from the index set {0, ..., n-1} into {0, ..., k-1}. If argMap[i] = j, this indicates that when matching against the rule type, the instantiation tⱼ of yⱼ should be substituted for xᵢ.

Instances For
Equations
Equations
Instances For
Equations
Instances For
Equations
Instances For
def Aesop.forEachExprInGoalCore {ω : Type} {m : } [STWorld ω m] [MonadLiftT (ST ω) m] [] [] (mvarId : Lean.MVarId) (g : ) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
@[always_inline]
def Aesop.forEachExprInGoal' {ω : Type} {m : } [STWorld ω m] [MonadLiftT (ST ω) m] [] [] (mvarId : Lean.MVarId) (g : ) :
Equations
Instances For
@[always_inline]
def Aesop.forEachExprInGoal {ω : Type} {m : } [STWorld ω m] [MonadLiftT (ST ω) m] [] [] (mvarId : Lean.MVarId) (g : ) :
Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
def Aesop.RulePattern.elab (stx : Lean.Term) (ruleType : Lean.Expr) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For