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.

pattern : Lean.Meta.AbstractMVarsResult
An expression of the form λ y₀ ... yₖ, p representing the pattern.
argMap : Array (Option Nat)
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ᵢ.
levelArgMap : Array (Option Nat)
A partial map from the level metavariables occurring in the rule to the pattern's level params.
discrTreeKeys : Array Lean.Meta.DiscrTree.Key
Discrimination tree keys for p.