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ᵢ that occur in p. 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 : 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ᵢ.

Instances For
    Equations
    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
        @[always_inline]
        def Aesop.forEachExprInGoal' {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] [MonadControlT Lean.MetaM m] [MonadLiftT Lean.MetaM m] (mvarId : Lean.MVarId) (g : Lean.Exprm Bool) :
        Equations
        Instances For
          @[always_inline]
          def Aesop.forEachExprInGoal {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] [MonadControlT Lean.MetaM m] [MonadLiftT Lean.MetaM m] (mvarId : Lean.MVarId) (g : Lean.Exprm Unit) :
          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
                  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
                          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