structure Aesop.RulePattern : Type

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ᵢ.

instance Aesop.instInhabitedRulePattern : Inhabited Aesop.RulePattern

Equations

• Aesop.instInhabitedRulePattern = { default := { pattern := default, argMap := default } }

def Aesop.RulePattern.open (pat : Aesop.RulePattern) : Lean.MetaM (Array Lean.MVarId × Lean.Expr)

Equations

• pat.open = do let __discr ← Lean.Meta.openAbstractMVarsResult pat.pattern match __discr with | (mvarIds, fst, p) => pure (Array.map (fun (x : Lean.Expr) => x.mvarId!) mvarIds, p)

def Aesop.RulePatternInstantiation : Type

Equations

• Aesop.RulePatternInstantiation = Array Lean.Expr

instance Aesop.instRulePatternInstantiationInhabited : Inhabited Aesop.RulePatternInstantiation

Equations

• Aesop.instRulePatternInstantiationInhabited = Array.instInhabited

instance Aesop.instRulePatternInstantiationBEq : BEq Aesop.RulePatternInstantiation

Equations

• Aesop.instRulePatternInstantiationBEq = Array.instBEq

instance Aesop.instRulePatternInstantiationHashable : Hashable Aesop.RulePatternInstantiation

Equations

• Aesop.instRulePatternInstantiationHashable = instHashableArray

def Aesop.RulePatternInstantiation.toArray : Aesop.RulePatternInstantiation → Array Lean.Expr

Equations

• Aesop.RulePatternInstantiation.toArray = id

instance Aesop.instEmptyCollectionRulePatternInstantiation : EmptyCollection Aesop.RulePatternInstantiation

Equations

• Aesop.instEmptyCollectionRulePatternInstantiation = { emptyCollection := #[] }

def Aesop.forEachExprInGoalCore {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] [MonadControlT Lean.MetaM m] [MonadLiftT Lean.MetaM m] (mvarId : Lean.MVarId) (g : Lean.Expr → m Bool) : Lean.MonadCacheT Lean.Expr Unit m Unit

Equations

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

@[always_inline]

def Aesop.forEachExprInGoal' {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] [MonadControlT Lean.MetaM m] [MonadLiftT Lean.MetaM m] (mvarId : Lean.MVarId) (g : Lean.Expr → m Bool) : m Unit

Equations

• Aesop.forEachExprInGoal' mvarId g = (Aesop.forEachExprInGoalCore mvarId g).run

@[always_inline]

def Aesop.forEachExprInGoal {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] [MonadControlT Lean.MetaM m] [MonadLiftT Lean.MetaM m] (mvarId : Lean.MVarId) (g : Lean.Expr → m Unit) : m Unit

Equations

• Aesop.forEachExprInGoal mvarId g = Aesop.forEachExprInGoal' mvarId fun (e : Lean.Expr) => do g e pure true

def Aesop.matchRulePatternsCore (pats : Array (Aesop.RuleName × Aesop.RulePattern)) (mvarId : Lean.MVarId) : StateRefT' IO.RealWorld (Std.HashMap Aesop.RuleName (Std.HashSet Aesop.RulePatternInstantiation)) Lean.MetaM Unit

Equations

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

def Aesop.matchRulePatterns (pats : Array (Aesop.RuleName × Aesop.RulePattern)) (mvarId : Lean.MVarId) : Lean.MetaM (Std.HashMap Aesop.RuleName (Std.HashSet Aesop.RulePatternInstantiation))

Equations

• Aesop.matchRulePatterns pats mvarId = (fun (x : Unit × Std.HashMap Aesop.RuleName (Std.HashSet Aesop.RulePatternInstantiation)) => x.snd) <$> (Aesop.matchRulePatternsCore pats mvarId).run ∅

def Aesop.RulePattern.getInstantiation {m : Type → Type} [Monad m] [Lean.MonadError m] (pat : Aesop.RulePattern) (inst : Aesop.RulePatternInstantiation) (argIndex : Nat) : m (Option Lean.Expr)

Equations

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

def Aesop.RulePattern.openRuleType (pat : Aesop.RulePattern) (inst : Aesop.RulePatternInstantiation) (type : Lean.Expr) : Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr × Std.HashSet Lean.MVarId)

Equations

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

def Aesop.RulePattern.specializeRule (pat : Aesop.RulePattern) (inst : Aesop.RulePatternInstantiation) (rule : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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

def Aesop.RulePattern.elab (stx : Lean.Term) (ruleType : Lean.Expr) : Lean.Elab.TermElabM Aesop.RulePattern

Equations

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

def Aesop.RulePattern.elab.fvarsToMVars (fvars : Array Lean.Expr) (e : Lean.Expr) : Lean.MetaM (Lean.Expr × Array Lean.MVarId)

Equations

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

def Aesop.RulePattern.elab.setMVarUserNamesToUniqueNames (e : Lean.Expr) : Lean.MetaM Unit

Equations

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

def Aesop.RulePattern.elab.abstractMVars' (e : Lean.Expr) : Lean.MetaM (Lean.Meta.AbstractMVarsResult × Std.HashMap Lean.MVarId Nat)

Equations

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