Documentation

Aesop.RuleTac.Apply

source
def Aesop.RuleTac.applyConst (decl : Lean.Name) (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) (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