Documentation

Aesop.RuleTac.Apply

source
def Aesop.RuleTac.applyExpr' (goal : Lean.MVarId) (e : Lean.Expr) (n : Lean.Name) (pat? : Option Aesop.RulePattern) (patInst : Aesop.RulePatternInstantiation) (md : Lean.Meta.TransparencyMode) (generateScript : Bool) :
Lean.MetaM Aesop.RuleApplication
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Aesop.RuleTac.applyExpr (goal : Lean.MVarId) (e : Lean.Expr) (n : Lean.Name) (pat? : Option Aesop.RulePattern) (patInsts : Lean.HashSet Aesop.RulePatternInstantiation) (md : Lean.Meta.TransparencyMode) (generateScript : Bool) :
    Lean.MetaM Aesop.RuleTacOutput
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Aesop.RuleTac.applyConst (decl : Lean.Name) (pat? : Option Aesop.RulePattern) (md : Lean.Meta.TransparencyMode) :
      Aesop.RuleTac
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Aesop.RuleTac.applyFVar (userName : Lean.Name) (pat? : Option Aesop.RulePattern) (md : Lean.Meta.TransparencyMode) :
        Aesop.RuleTac
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Aesop.RuleTac.applyConsts (decls : Array Lean.Name) (md : Lean.Meta.TransparencyMode) :
          Aesop.RuleTac
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For